主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
黄涛,钱军,倪彬.Trace 演算.软件学报,1999,10(8):790-799
Trace 演算
Trace Calculus
投稿时间:1997-12-12  修订日期:1998-09-04
DOI:
中文关键词:  Trace演算,对象标记,动作,踪迹,公理化,可靠性.
英文关键词:Trace calculus, object signature, action, trace, axiomatization, Soundness.
基金项目:本文研究得到国家自然科学基金和国家863高科技项目基金资助.
作者单位
黄涛 中国科学院软件研究所计算机科学开放实验室,北京,100080 
钱军 中国科学院软件研究所对象技术中心,北京,100080 
倪彬 中国科学院软件研究所对象技术中心,北京,100080 
摘要点击次数: 2671
全文下载次数: 2374
中文摘要:
      文章定义了基于踪迹(trace)的逻辑语言LTrace,它是一阶线性时序逻辑语言的扩充,同时也是“对象演算”研究工作的基础.Trace演算所述的“对象”用来刻画具有内部状态和外部行为的动态实体,语法上由对象标记表示.对象标记Ω=(S,F,A,E)包含4个部分:数据类型S、函数F、属性A和动作E.Σ=(S,F)构成通常代数规范意义下的标记,可将动作看成一广义数据类型,从而得到标记Σ的动作扩充ΣE.对象标记的语义解释结构由关于标记ΣE的代数、映射和动作与踪迹的关系定义.ΣE-代数给出关于数据参数的解释;映射给出属性在动作踪迹中所取的值;而动作与踪迹的关系则给出执行一有限踪迹以后该动作是否允许执行.在定义了Trace演算的语法和语义之后,文章给出了Trace演算的公理系统及其可靠性证明.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利