axiomatic semantics

Also found in: Wikipedia.

axiomatic semantics

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.
References in periodicals archive ?
Axiomatic semantics: An axiomatic semantics for a language specifies "a mapping of a set of descriptions in [that] language into a logical theory expressed in first-order predicate calculus" (p.
There are many examples of informally expressed semantics, usually found in specification documents written in (often highly technical) natural language: (1) the meaning of terms in the Dublin core; (11) (2) the meaning of tags in HTML such as <h2>, which means second-level header; (3) the meaning of expressions in modeling languages such as the UNIFIED MODELING LANGUAGE (UML); (12) (4) the informal semantics in the original specification of RDF SCHEMA; (13) (5) the model theory (formal semantics) of RDF SCHEMA that is developed subsequently (does not include the axiomatic semantics that is expressed in a formal language).
Operational semantics provide an abstract implementation-oriented account of program meaning, denotational semantics give a more abstract mathematical account, and axiomatic semantics focus on partial correctness issues (see Nielson and Nielson [1992] and Tennent [1991] for a thorough discussion).