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

Re: Using MEASURE-INDUCT




Darryl:
  If I read your message correctly, you have a queue of
elements in decreasing order.  The nextState operation 
removes the head of the queue and can add smaller elements
to the tail to preserve the queue ordering.  You'd like
to use measure induction to show that any item added to the
queue eventually appears at the head of the queue.

For the induction to work,  you need a suitably general induction
statement and an appropriate measure.

1. You might need to prove the statement:
  member(x, q) IMPLIES eventually(LAMBDA qq: head(qq) = x, q).

The reason for this generalization is that in the next state to q,
x may no longer be the most recently added element.  

2. The measure "Value(q) - x" could be used.  The lemma:
 member(x, q) IMPLIES x <= Value(q) can be used to show that this
 measure is sensible, i.e., nonnegative.  It is therefore
well-founded and decreases with each invocation of eventually until
x is at the head of the queue.  

I have a very preliminary theory of queues implemented with lists.
It never progressed to the stage where it could be inflicted
on others.  I'd be interested if someone else has a well worked
out theory of queues.

-Shankar

> From:    Darryl Scott Dieckman <ddieckma@ececs.uc.edu>
> Subject: Using MEASURE-INDUCT
> Date:    Tue, 28 Apr 1998 17:31:27 EDT
> To:      pvs-help@csl.sri.com
> 
> 
> 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
>