UNC-CH COMP 410

ADT Axiomatic Semantics

STACK of E (LIFO list)

Algebraic Semantics (Guttag's Method)

STACK is the type we are defining
The list/stack contains elements of some type E

signatures (operations and types of parameters/return value)

   new:             --> STACK       (canonical constructor)
   push: STACK x E  --> STACK       (canonical constructor)
   pop: STACK       --> STACK
   top: STACK       --> E
   size: STACK      --> nat   (naturals, int >=0 )
   empty: STACK     --> boolean

axioms (behavior)

  size(new) = 0
  size(push(S,e)) = size(S) + 1

  empty(new) = true
  empty(push(S,e)) = false

  top(new) = error                 
  top(push(S,e)) = e

  pop(new) = new
  pop(push(S,e)) = S

SML representation of the semantics

this version is stack of int... works on ints only

(* canonical ops are done as SML user-defined datatype *)


datatype STI = 
   New  
   | push of STI * int ;

(* non-canonical ops are done using partial function definitions,
   more-or-less one per axiom
*)

fun size (New) = 0
  | size (push(S,i)) = size(S)+1;

fun pop (New) = New
  | pop (push(S,i)) = S ;

fun empty (New) = true
  | empty (S) = (size(S)=0) ;

exception topEmptyStack;

fun top (New) = raise topEmptyStack 
  | top (push(S,i)) = i ;



(*---------------------------------------*)
(*   test data points                    *)
(*---------------------------------------*)

  val s0 = New;
  val s1 = push(s0,10);
  val s2 = push(s1,20);
  val s3 = push(s2,30);

(*---------------------------------------*)
(*   test cases                          *)
(*---------------------------------------*)

  size(s2) = 2;
  size(s0) = 0;
  size(s3) = 3;
  top(s2) = 20;
  top(s1) = 10;

  size(push(s3,40)) = size(s3) + 1;
  size(push(s3,40)) = 4;

  size(pop(s3)) = size(s3) - 1;
  size(pop(s3)) = 2;
  size(pop(s1)) = 0;
  size(pop(New)) = 0;

  top(pop(s3)) = 20;
  top(pop(s2)) = 10;
  top(pop(s1));

  top(pop(push(push(pop(push(s3,40)),50),60))) = 50;
  size(pop(push(push(pop(push(s3,40)),50),60))) = 4;

SML representation of the semantics

this version is stack of any type... the datatype defn is parameterized

datatype ('e) STACK = 
   New  
   | push of ('e) STACK  * 'e ;

(* non-canonical ops are done using partial function definitions,
   more-or-less one per axiom
*)

fun size (New) = 0
  | size (push(S,i)) = size(S)+1;

fun pop (New) = New
  | pop (push(S,i)) = S ;

fun empty (New) = true
  | empty (S) = (size(S)=0) ;

exception topEmptyStack;

fun top (New) = raise topEmptyStack 
  | top (push(S,i)) = i ;