axiomatic semantics

Computing Dictionary

axiomatic semantics definition

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)
The Free On-line Dictionary of Computing, © Denis Howe 2010 http://foldoc.org
Cite This Source
Explore Dictionary.com
More from Thesaurus.com
Synonyms and Antonyms for axiomatic semantics
More from Reference.com
Search for articles containing axiomatic semantics
Dictionary.com Word FAQs

Dictionary.com presents 366 FAQs, incorporating some of the frequently asked questions from the past with newer queries.

Copyright © 2014 Dictionary.com, LLC. All rights reserved.
  • Please Login or Sign Up to use the Recent Searches feature