计算机科学与探索 ›› 2010, Vol. 4 ›› Issue (1): 20-28.DOI: 10.3778/j.issn.1673-9418.2010.01.002

• 学术研究 • 上一篇    下一篇

O-表达式的性质定义与规范

袁崇义1,2,赵 文1,2,3,高 昕1,2,黄 雨1,2,3+   

  1. 1. 北京大学 教育部高可信软件技术重点实验室,北京 100871
    2. 北京大学 信息科学技术学院,北京 100871
    3. 北京大学 软件工程国家工程研究中心,北京 100871
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2010-01-15 发布日期:2010-01-15
  • 通讯作者: 黄 雨

Definitions and Specifications of O-expression Properties

YUAN Chongyi1,2, ZHAO Wen1,2,3, GAO Xin1,2, HUANG Yu1,2,3+   

  1. 1. Key Lab of High Confidence Software Technologies of MOE, Peking University, Beijing 100871, China
    2. School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China
    3. National Engineering Research Center for Software Engineering, Peking University, Beijing 100871, China
  • Received:1900-01-01 Revised:1900-01-01 Online:2010-01-15 Published:2010-01-15
  • Contact: HUANG Yu

摘要: 在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式。给出了此类表达式(O-表达式)的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式。具有明确运行目标的O-表达式称为独立O-表达式(stand-alone O-expression,saloe)。一个完整的程序可能由若干个saloe组成。给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。

关键词: O-表达式, 独立O-表达式, 安全性, 进展性, 不变性, 程序规范

Abstract: In the programming paradigm proposed in the series, assignments have become operations on physical objects and programs have turned out to be expressions of operations on physical objects (O-expressions). Safety properties and progress properties of O-expressions are formally defined, and formal specifications based on these properties are proposed with examples. An O-expression with an explicit goal is said to be a stand-alone O-expression (saloe for short) and a complete program may consist of more than one saloe. A theorem on how to deduce properties of a program from formal specifications of its constituent saloe is given. Many examples can be found for exploring formal definitions of program properties.

Key words: O-expression, stand-alone O-expression (saloe), safety, progress property, invariant, program spe-cification

中图分类号: