資料來源 : Free On-Line Dictionary of Computing

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}.
     
        (1995-11-09)