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

摘要：

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

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

所属期刊栏目：4

分类号：TP311(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant No.60803014;the National High-Tech Research and Development Plan of China under Grant No.2006AA012160国家高技术研究发展计~863;the National Research Foundation for Doctoral Program of Higher Education of China under Grant No.200800011017

在线出版日期：2010-03-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：20-28