Definition: Defining the behavior of an abstract data type with axioms.
Aggregate parent (I am a part of or used in ...)
stack, bag, dictionary, priority queue, queue, set, cactus stack.
For example, the abstract data type stack has the operations new(), push(v, S) and popOff(S), among others. These may be defined with the following axioms.
The second axiom says that if we push a value onto a stack then pop it off, the result is the same stack. The "=" can be seen as a rewrite operation. The axiom "X = Y" means any time we see X, we can rewrite it to be Y. X may contain variables representing subexpressions. What is the meaning of "popOff(push(1776, new()))"? The second axiom says it means the same as new().
The third axiom assigns meaning to expressions like top(push(1, push(2, new()))): it is 1. This is reasonable, since the top element is the latest one pushed. A series of push and popOff operations and a top operation may be reduced with these axioms.
What stack does new() return, then? We still haven't said; top(new()) is just not defined. But that is how a stack works: the top of an empty stack is not defined. So our formalism corresponds to our mental notion of a stack. If we want to, we can add more axioms for richer semantics, as is done in the stack entry.
If you have suggestions, corrections, or comments, please get in touch with Paul E. Black.
Entry modified 24 August 2005.
HTML page formatted Fri Mar 25 16:20:34 2011.
Cite this as:
Paul E. Black, "axiomatic semantics", in Dictionary of Algorithms and Data Structures [online], Paul E. Black, ed., U.S. National Institute of Standards and Technology. 24 August 2005. (accessed TODAY) Available from: http://www.nist.gov/dads/HTML/axiomaticSemantics.html