| O-表达式的性质定义与规范 |
| |
| 引用本文： | 袁崇义,赵文,高昕,黄雨.O-表达式的性质定义与规范[J].计算机科学与探索,2010,4(1):20-28. |
| |
| 作者姓名： | 袁崇义 赵文 高昕 黄雨 |
| |
| 作者单位： | 1. 北京大学教育部高可信软件技术重点实验室,北京100871;北京大学信息科学技术学院,北京100871
2. 北京大学教育部高可信软件技术重点实验室,北京100871;北京大学信息科学技术学院,北京100871;北京大学软件工程国家工程研究中心,北京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;;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-表达式 安全性 进展性 不变性 程序规范 |
| 修稿时间： | |
Received 2009-07Definitions and Specifications of O-expression Properties |
| |
| YUAN Chongyi,ZHAO Wen,GAO Xin,HUANG Yu.Received 2009-07Definitions and Specifications of O-expression Properties[J].Journal of Frontier of Computer Science and Technology,2010,4(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 salo... |
| |
| Keywords: | O-expression stand-alone O-expression (saloe) safety progress property invariant program specification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学与探索》浏览原始摘要信息 |
|
点击此处可从《计算机科学与探索》下载全文 |
