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

• 作者: 袁崇义 赵文 高昕 黄雨
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: O-表达式 独立O-表达式 安全性 进展性 不变性 程序规范
• 年，卷（期）: 2010,（1）
• 所属期刊栏目: 学术研究
• 页码范围: 20-28
• 页数: 9页
• 分类号: TP311
• 字数: 1020字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.2010.01.002

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	赵文	北京大学教育部高可信软件技术重点实验室	26	672	8.0	25.0
10	袁崇义	北京大学教育部高可信软件技术重点实验室	17	173	7.0	12.0
14	高昕	北京大学教育部高可信软件技术重点实验室	2	6	1.0	2.0