UNC-CH COMP 410

ADT Axiomatic Semantics

LISP LIST of E

LLIST is the type we are defining
the list contains elements of some type E

signatures

   new   :                --> LLIST        (canonical constructor)
   add   : LLIST x E      --> LLIST        (canonical constructor)

   first : LLIST          --> E U error
   rest  : LLIST          --> LLIST
   size  : LLIST          --> nat           (naturals, int >=0 )
   empty : LLIST          --> boolean

   cons  : LLIST x LLIST  --> LLIST


axioms

   size(new) = 0
   size(add(LL,e)) = size(LL)+1

   empty(new) = true
   empty(add(LL,e)) = false

   first(new) = error
   first(add(LL,e)) = e

   rest(new) = new
   rest(add(LL,e)) = LL


   cons(new,L) = L
   cons(add(L1,e),L2) =  add(cons(L1,L2),e)