A trace-based logic language: L_Trace is defined in this paper, which is an extension of the first-order linear temporal logic and serves as cornerstone of the works ——Object Calculus. The objects in trace calculus represent the dynamic entities endowed with a local state and external actions, and described by an object signature in syntax. An object signature is a 4-tuple Ω=(S,F,A,E) in which S stands for a set of data sorts, F functions, A attributes and E actions. Σ=(S,F) is nothing but a usual signature in the context of algebraic specification. It can be extended to ΣE with the action regarded as a special data sort. The semantics of trace calculus is defined by an object signature semantic interpreting structure I=(A,F,E), which consists of a ΣE- Algebra A giving an interpretation about data parameters, a mapping F evaluating the attributes on an action trace, and a relation E giving a relationship between actions and a trace. Finally, we contribute an axiom system of our trace calculus and outlines its proof of soundness after we define the syntax and semantics of the trace calculus.