|axiomatic semantics||computing dictionary|
<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.
(01 Mar 1995)
|Bookmark with:||word visualiser||Go and visit our forums|