CAJ | 학술논문

在所提出的程序设计方法中,赋值是物理对象上的操作,而程序则是这种操作的表达式.给出了此类表达式(O-表达式)的安全性和进展性性质的形式化定义,用实例说明了基于这些性质的形式化程序规范的模式.具有明确运行目标的O-表达式称为独立O-表达式(stand-alone O-expression,saloe).一个完整的程序可能由若干个saloe组成.给出了一个定理,指出如何从这些saloe的性质导出完整性程序的性质.用大量实例阐明了程序性质的形式定义.
재소제출적정서설계방법중,부치시물리대상상적조작,이정서칙시저충조작적표체식.급출료차류표체식(O-표체식)적안전성화진전성성질적형식화정의,용실례설명료기우저사성질적형식화정서규범적모식.구유명학운행목표적O-표체식칭위독립O-표체식(stand-alone O-expression,saloe).일개완정적정서가능유약간개saloe조성.급출료일개정리,지출여하종저사saloe적성질도출완정성정서적성질.용대량실례천명료정서성질적형식정의.
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 0-expressions are formally defined, and formal specifications based on these properties are proposed with examples. An 0-expression with an explicit goal is said to be a stand-alone 0-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.