title: Axiomatic Semantics

abstract:
In axiomatic semantics, the meaning of a program is based on assertions about relationships that remain
the same each time the program executes. The relation between an initial assertion and a final assertion following a piece of code captures the essence of the semantics of the code. Another piece of code that defines the algorithm slightly differently yet produces the same final assertion will be semantically equivalent provided any initial assertions are also the same. The proofs that the assertions are true do not rely on any particular architecture for the underlying machine; rather they depend on the relationships between the values of the variables. Although individual values of variables change as a program executes, certain relationships among them remain the same. These invariant relationships form the assertions that express the semantics of the program.