赋值:物理对象上的操作(英文)  

Assignment: operation on a physical object

作　　者：袁崇义[1] 

机构地区：[1]北京大学信息科学技术学院,北京100871

出　　处：《计算机科学与探索》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~~

摘　　要：研究了命令式程序的形式语义。赋值被看成当作物理对象的变量上的操作。变量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.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]