|
|
types
Stack, Integer, Boolean
operations
create : --> Stack
push : Stack x Integer --> Stack
pop : Stack --> Stack
top : Stack --> Integer
isEmpty : Stack --> Boolean
preconditions
pre-pop(s) = not isEmpty(s)
pre-top(s) = not isEmpty(s)
var
s : Stack;
i : Integer;
axioms
isEmpty(create()) = true
isEmpty(push(s,i)) = false
pop(push(s,i)) = s
top(push(s,i)) = i
|
|
| Letzte Änderung: 31.12.2006 | © Prof. Dr. Uwe Schmidt |