axiomatic semantics


axiomatic semantics

(theory)A set of assertions about properties of a system andhow they are effected by program execution. The axiomaticsemantics of a program could include pre- and post-conditionsfor operations. In particular if you view the program as astate transformer (or collection of state transformers), theaxiomatic semantics is a set of invariants on the state whichthe state transformer satisfies.

E.g. for a function with the type:

sort_list :: [T] -> [T]

we might give the precondition that the argument of thefunction is a list, and a postcondition that the return valueis a list that is sorted.

One interesting use of axiomatic semantics is to have alanguage that has a finitely computable sublanguage that isused for specifying pre and post conditions, and then have thecompiler prove that the program will satisfy those conditions.

See also operational semantics, denotational semantics.