共 2 条
Trace演算
被引：4
作者：
黄涛
钱军
倪彬
机构：
[1] 中国科学院软件研究所计算机科学开放研究实验室!北京，
[2] 中国科学院软件研究所对象技术中心!北京，
来源：
关键词：
Trace演算;
对象标记;
动作;
踪迹;
公理化;
可靠性;
D O I：
10.13328/j.cnki.jos.1999.08.002
中图分类号：
TP311.5 [软件工程];
学科分类号：
摘要：
文章定义了基于踪迹（trace）的逻辑语言Trace，它是一阶线性时序逻辑语言的扩充，同时也是“对象演算”研究工作的基础．Trace演算所述的“对象”用来刻画具有内部状态和外部行为的动态实体，语法上由对象标记表示．对象标记Ω＝（S，F，A，E）包含4个部分；数据类型S、函数F、属性A和动作E．∑＝（S，F）构成通常代数规范意义下的标记，可将动作看成一个广义数据类型，从而得到标记∑的动作扩充∑E．对象标记的语义解释结构由关于标记∑E的代数、映射和动作与踪迹的关系来定义．∑E－代数给出关于数据参数的解释；映射给出属性在动作踪迹中所取的值；而动作与踪迹的关系则给出执行一有限踪迹以后该动作是否允许执行．在定义了Trace演算的语法和语义之后，文章给出了Trace演算的公理系统及其可靠性证明．
引用
收藏
页码：790 / 799
页数：10
相关论文