[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Using MEASURE-INDUCT




I would like to prove somethings about a Queue specification that I
have written, but am running into difficulty.  Here is a quick
synopsis of what I am trying to do.  

1. I have a theory of queues
2. I am using a queue to represent a list of items in my specification
3. I have a nextState function that takes the current queue and 
   may add items to the end of the queue and returns the new queue
4. I have following definition which says that eventually a 
   state will occur that satisfies the given predicate given the 
   initial state.

eventually(p : [Queue->bool], q : Queue): RECURSIVE bool = 
  IF p(q) THEN
    TRUE
  ELSIF empty?(q) THEN
    FALSE
  ELSE
    eventually(p, nextState(q))
  ENDIF
  MEASURE (value(q))

The TCC's for eventually are satisfied, because value(q) will 
always decrease.

Hopefully I have given enough information to get some help with the 
next question.  

I want to prove that if I add an item to the end of any queue, that 
that item will eventually become the first item in the queue.  I know
that this is true, because nextState always removes and item, and 
can only append items to the end of the queue.

I believe that I want to use one of the MEASURE-xxx strategies, but 
cannot figure out how to get the measure function for 'eventually'
to appear.  Another question, does anyone have a good specification
for a queue?

Thanks 
Darryl Dieckman