Journal of Frontiers of Computer Science and Technology ›› 2008, Vol. 2 ›› Issue (5): 487-499.DOI: 10.3778/j.issn.1673-9418.2008.05.004

• 学术研究 • Previous Articles     Next Articles

Assignment: Operation on a Physical Object

YUAN Chongyi+   

  1. School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-10-06 Published:2008-10-06
  • Contact: YUAN Chongyi



  1. 北京大学 信息科学技术学院,北京 100871
  • 通讯作者: 袁崇义

Abstract: 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 a mathematical expression. As a physical object, x allows its value to be observed and/or changed by read/write operations applied on it. Thus, assignments are in fact write-operations applied on physical objects. A read-operation is the reverse of write-operation. Operations 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.

Key words: assignment, imperative program, physical object, operation on physical object, operation axiom, axiom semantics

摘要: 研究了命令式程序的形式语义。赋值被看成当作物理对象的变量上的操作。变量x一方面是个可以容纳数据值的物理对象,另一方面当它出现在数学表达式中时又代表它所容纳的值。作为物理对象,变量x允许它的值用读/写操作来观察或改变,读操作则是写操作的逆操作。事实上赋值就是对物理对象施加写操作。提出了与单变量赋值、多重赋值、顺序赋值及条件赋值等相对应的操作,提出了这些操作应服从的公理,并给出了用这些公理证明程序性质的实例。

关键词: 赋值, 命令式程序, 物理对象, 物理对象上的操作, 操作公理, 公理语义