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

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