Assignment: operation on a physical object
Chongyi Yuan · Jisuanji kexue yu tansuo · 2008
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.