07/07/08 23:42:28
【 補足 】スタックの抽象データ型の定義
TYPES
STACK[X]
FUNCTIONS
empty: STACK[X] → BOOLEAN
スタックを入力として与えて、真偽を返す関数である
new: → STACK[X]
入力を与えずに、呼ばれると新しいスタックを返す関数である
push: X × STACK[X] → STACK[X]
スタックにいれる要素とスタックを与えて、要素が入れられたスタックを返す関数である
pop: STACK[X] ⇒ STACK[X]
スタックを与えて、(先頭の要素が取り除かれた)スタックを返す
top: STACK[X] ⇒ X
スタックを与えて、(先頭の)要素を返す関数である
PRECONDITIONS
pre pop(s:STACK[X]) = (not empty(s))
pre top(s:STACK[X]) = (not empty(s))
AXIOMS
For all x:X, s:STACK[X]
empty(new())
not empty(push(x,s))
top(push(x,s)) = x
pop(push(x,s)) = s