[ Course Documents ] : [ Semantics ]

Previous Contents Next Keyword Index

Axiomatic Semantics

• Based on formal logic (first order predicate calculus)

• Original purpose: formal program verification

• Approach: Define axioms or inference rules for each statement type in the language

• Such an inference rule allows one to transform expressions to other expressions

• The expressions are called assertions, and state the relationships and constraints among variables that are true at a specific point in execution

• An assertion before a statement is called a precondition

• An assertion following a statement is a postcondition