摘要
研究了命令式程序的形式语义。赋值被看成当作物理对象的变量上的操作。变量x一方面是个可以容纳数据值的物理对象,另一方面当它出现在数学表达式中时又代表它所容纳的值。作为物理对象,变量x允许它的值用读/写操作来观察或改变,读操作则是写操作的逆操作。事实上赋值就是对物理对象施加写操作。提出了与单变量赋值、多重赋值、顺序赋值及条件赋值等相对应的操作,提出了这些操作应服从的公理,并给出了用这些公理证明程序性质的实例。
This paper focuses on formal semantics of imperative programs. Assignments are viewed as operations on variables considered as a physical objects. Variable x is, on the one hand, a physical object which is able to hold a data value while on the other hand, it represents the value it currently holds when it appears in by read/ objects. a mathematical write operations expression. As a physical object, applied on it. Thus, assignments A read-operation is the reverse of write-operation x allows its are in fact Operations value to be observed and/or write-operations applied on changed physical corresponding to assignments on single variable, multi-variable sequential assignments and conditional assignments etc, are proposed. Axioms on these operations are also proposed as formal semantics of assignments, and examples are given to show how to verify program properties with these axioms.
出处
《计算机科学与探索》
CSCD
2008年第5期487-499,共13页
Journal of Frontiers of Computer Science and Technology
基金
the National Grand Fundamental Research 973 Program of China under Grant No.2002CB312004,2002CB312006
the National High-Tech Research and Development Plan of China under Grant No.2006AA04A119,2006AA01Z160~~
关键词
赋值
命令式程序
物理对象
物理对象上的操作
操作公理
公理语义
assignment
imperative program
physical object
operation on physical object
operation axiom
axiom semantics
