from
The Free On-line Dictionary of Computing (8 July 2008)
axiomatic semantics
<theory> A set of assertions about properties of a system and
how they are effected by program execution. The axiomatic
semantics of a program could include pre- and post-conditions
for operations. In particular if you view the program as a
state transformer (or collection of state transformers), the
axiomatic semantics is a set of invariants on the state which
the state transformer satisfies.
E.g. for a function with the type:
sort_list :: [T] -> [T]
we might give the precondition that the argument of the
function is a list, and a postcondition that the return value
is a list that is sorted.
One interesting use of axiomatic semantics is to have a
language that has a {finitely computable} sublanguage that is
used for specifying pre and post conditions, and then have the
compiler prove that the program will satisfy those conditions.
See also {operational semantics}, {denotational semantics}.
(1995-11-09)