| 摘要: |
| 文章定义了基于踪迹(trace)的逻辑语言LTrace,它是一阶线性时序逻辑语言的扩充,同时也是“对象演算”研究工作的基础.Trace演算所述的“对象”用来刻画具有内部状态和外部行为的动态实体,语法上由对象标记表示.对象标记Ω=(S,F,A,E)包含4个部分:数据类型S、函数F、属性A和动作E.Σ=(S,F)构成通常代数规范意义下的标记,可将动作看成一广义数据类型,从而得到标记Σ的动作扩充ΣE.对象标记的语义解释结构由关于标记ΣE的代数、映射和动作与踪迹的关系定义.ΣE-代数给出关于数据参数的解释;映射给出属性在动作踪迹中所取的值;而动作与踪迹的关系则给出执行一有限踪迹以后该动作是否允许执行.在定义了Trace演算的语法和语义之后,文章给出了Trace演算的公理系统及其可靠性证明. |
| 关键词: Trace演算,对象标记,动作,踪迹,公理化,可靠性. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金和国家863高科技项目基金资助. |
|
| Trace Calculus |
|
HUANG Tao,QIAN Jun,NI Bin
|
| Abstract: |
| A trace-based logic language: LTrace 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. |
| Key words: Trace calculus, object signature, action, trace, axiomatization, Soundness. |
