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

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