Assignment 2: Axiomatic Semantics
(due Tues. Sep. 18, by 11:00am, classtime)
       
1) Write an axiomatic semantic definition for a
Bounded Queue of E (BQUE).
A BQUE is created with some finite size (>0)
and when an enq operation is done, if the BQUE is full
then nothing changes... the item is not added to the BQUE and
no items in the BQUE are removed.
       
You can use the axioms
we developed in class for a Bounded Stack (BST) as a model;
obviously there will be some changes in the axioms, since
a BQUE behaves differently from a BST.
Use these signatures:
BQUE of E
new: pos --> BQUE (here, pos is int > 0)
enq: BQUE x E --> BQUE
deq: BQUE --> BQUE
front: BQUE --> E
back: BQUE --> E
size: BQUE --> nat (naturals, int >=0 )
max: BQUE --> pos
empty: BQUE --> boolean
full: BQUE --> boolean
       
2) Write an axiomatic semantic definition of the basic LIST
we studied in class. This will be similar to the axioms for
STACK (and QUEUE) but a bit more complex, since LIST has operations
that manipulate the inner elements as well as the ends.
Use these signatures:
LIST of E
new: --> LIST
add: LIST x E x nat --> LIST (here, nat means int >=0)
del: LIST x nat --> LIST
get: LIST x nat --> E
size: LIST --> nat
empty: LIST --> boolean