| O-表达式的性质定义与规范（英文） |
| |
| 引用本文： | 袁崇义,赵文,高昕,黄雨.O-表达式的性质定义与规范（英文）[J].计算机与生活,2010(1):20-28. |
| |
| 作者姓名： | 袁崇义 赵文 高昕 黄雨 |
| |
| 作者单位： | [1]北京大学教育部高可信软件技术重点实验室,北京100871 [2]北京大学信息科学技术学院,北京100871 [3]北京大学软件工程国家工程研究中心,北京100871 |
| |
| 基金项目： | The National Natural Science Foundation of China under Grant No.60803014（国家自然科学基金）; the National High-Tech Researchand Development Plan of China under Grant No.2006AA01Z160; （国家高技术研究发展计划（863））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的性质导出完整性程序的性质。用大量实例阐明了程序性质的形式定义。
|
| 关 键 词： | O-表达式 独立O-表达式 安全性 进展性 不变性 程序规范 |
Definitions and Specifications of O-expression Properties |
| |
| YUAN Chongyi,ZHAO Wen,GAO Xin,HUANG Yu.Definitions and Specifications of O-expression Properties[J].Egamer,2010(1):20-28. |
| |
| Authors: | YUAN Chongyi ZHAO Wen GAO Xin HUANG Yu |
| |
| Affiliation: | 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 ) |
| |
| 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. |
| |
| Keywords: | O-expression stand-alone O-expression（saloe） safety progress property invariant program specification |
| 本文献已被 维普 等数据库收录！ |
