程序性质的描述及证明  

Description & Verification of a Program's Property

作　　者：官荷卿[1] 郭亮[1] 

机构地区：[1]中国科学院软件研究所计算机科学开放研究实验室,北京100080

出　　处：《计算机科学》2003年第3期146-148,共3页Computer Science

基　　金：国家自然科学基金YCK15028

摘　　要：XYZ/E是一种基于Manna-Pnueli线性时序逻辑的线性时序逻辑语青(LTLL),其主要特征为它在统一的时序逻辑框架下既能表示程序的静态规范(XYZ/AE)也能表示可执行代码(XYZ/EE),因此程序规范和程序可执行代码的语义一致性也就得以在时序逻辑框架下验证。对于顺序程序,XYZ系统提供了一套基于Hoare逻辑规则的验证工具XYZ/VERI。In this paper, we specify and implement the Dekker algorithm in XYZ/AE and XYZ/EE respectively, the semantic consistency between the specification and its implementation is also proved under the framework of temporal logic.

关 键 词：程序性质 程序设计 XYZ语言 AE语言 时序逻辑语言 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论] TP312[自动化与计算机技术—计算机科学与技术]