axiomatic semantics

1 definition found

axiomatic semantics - Free On-line Dictionary of Computing (26 May 2007) :

  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)