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

doi:10.3778/j.issn.1673-9418.2010.01.002

计算机科学与探索 ›› 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. 北京大学教育部高可信软件技术重点实验室，北京 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 Chongyi^1，2， ZHAO Wen^1，2，3， GAO Xin^1，2， HUANG Yu^1，2，3+

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

摘要/Abstract

摘要： 在所提出的程序设计方法中，赋值是物理对象上的操作，而程序则是这种操作的表达式。给出了此类表达式（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

中图分类号:

TP311

袁崇义1，2 ，赵文1，2，3 ，高昕1，2 ，黄雨1，2，3+ . O-表达式的性质定义与规范[J]. 计算机科学与探索, 2010, 4(1): 20-28.

YUAN Chongyi^1，2， ZHAO Wen^1，2，3， GAO Xin^1，2， HUANG Yu^1，2，3+. Definitions and Specifications of O-expression Properties[J]. Journal of Frontiers of Computer Science and Technology, 2010, 4(1): 20-28.

[1]	李彬，姜建国. 少数决：更安全的分布式一致性算法选举机制[J]. 计算机科学与探索, 2020, 14(10): 1693-1701.
[2]	张维珺，胡军，李宛倩，陈朔，石梦烨，唐红英. 安全关键系统需求形式化建模分析实例研究[J]. 计算机科学与探索, 2019, 13(8): 1295-1306.
[3]	李建民，俞惠芳，赵晨. UC安全的自认证盲签密协议[J]. 计算机科学与探索, 2017, 11(6): 932-940.
[4]	严宇，宋威. 颜色和纹理混合描述符图像检索方法[J]. 计算机科学与探索, 2017, 11(11): 1816-1825.
[5]	仵志鹏，胡军，陈松，石娇洁. 面向AltaRica模型的嵌入式系统安全性验证方法[J]. 计算机科学与探索, 2017, 11(1): 24-36.
[6]	张贵，张育平，陈海燕 . 面向适航认证的IMA架构安全性评估方法[J]. 计算机科学与探索, 2016, 10(8): 1063-1071.
[7]	鲍秋霜，张晋津. 直觉主义计算树逻辑中的安全性和活性[J]. 计算机科学与探索, 2016, 10(2): 163-172.
[8]	李全武，李玉惠，李勃，陈伊. 车脸定位及识别方法研究[J]. 计算机科学与探索, 2015, 9(6): 726-733.
[9]	杜长霄，李晓红，石红，冯志勇. J2EE应用软件的架构安全评估方法[J]. 计算机科学与探索, 2014, 8(5): 572-581.
[10]	何贤芒, 陈华辉, 肖仰华, 汪卫, 施伯乐. 动态数值敏感属性的数据隐私保护[J]. 计算机科学与探索, 2011, 5(8): 740-750.

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

Definitions and Specifications of O-expression Properties

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 10

编辑推荐

Metrics