O-表达式的性质定义与规范(英文)  

Definitions and Specifications of O-expression Properties

作　　者：袁崇义[1,2] 赵文[1,2,3] 高昕[1,2] 黄雨[1,2,3] 

机构地区：[1]北京大学教育部高可信软件技术重点实验室,北京100871 [2]北京大学信息科学技术学院,北京100871 [3]北京大学软件工程国家工程研究中心,北京100871

出　　处：《计算机科学与探索》2010年第1期20-28,共9页Journal of Frontiers of Computer Science and Technology

基　　金：The National Natural Science Foundation of China under Grant No.60803014;the National High-Tech Researchand Development Plan of China under Grant No.2006AA01Z160;the National Research Foundationfor Doctoral Program of Higher Education of China under Grant No.200800011017~~

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

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

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