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)
Nearby terms:
axiom « AXIOM* « Axiomatic Architecture Description
Language « axiomatic semantics » axiomatic
set theory » Axiom of Choice » Axiom of
Comprehension
|
