CS 3304: Comparative Languages
Semantics
[
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