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

【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.更多还原