2. Axiomatic Semantics

• The meaning of the programming language is defined implicitly by a logical calculus called program logic which provides a tool for the derivation of assertions of the form:

{Precondition} Program {Postcondition}

• Properties about program language constructs are defined and expressed with axioms and rules from logic. A property about a program is deduced by using the axioms and rules to construct a formal proof of the property.

• Axiomatic definitions tend to be abstract and are best used at the specification stage or to give documentation of language properties which are of interest to the user. Also used in algorithm derivation.

Previous slide

Next slide

Back to first slide

View graphic version