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

*To*: Darryl Scott Dieckman <ddieckma@ececs.uc.edu>*Subject*: Re: Using MEASURE-INDUCT*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Tue, 28 Apr 1998 16:27:13 -0700*cc*: pvs-help@csl.sri.com*In-reply-to*: Your message of "Tue, 28 Apr 1998 17:31:27 EDT." <199804282131.RAA02096@clifford.ececs.uc.edu>

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 >

**References**:**Using MEASURE-INDUCT***From:*Darryl Scott Dieckman <ddieckma@ececs.uc.edu>

- Prev by Date:
**Using MEASURE-INDUCT** - Next by Date:
**Re: latex problem** - Prev by thread:
**Using MEASURE-INDUCT** - Next by thread:
**PVS parser does not work** - Index(es):