特徴を表現する に使用してい る が FUNCTIONS で定義されて いる振る舞い み - AXIOMS - 任意 x:G, s:STACK[G]に対して 以下が成り立つ - 1. peek(push(s,x)) = x - 2. pop(push(s,x)) = s - 3. empty(new) - 4. not empty(push(s,x)) - PRECONDITIONS - peek(s: STACK[G]) require not empty(s) - pop(s: STACK[G]) require not empty(s) これがデータ構造を公開した振る舞い みで表現する使用記述である抽象データ型