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

*To*: pvs-help@csl.sri.com*Subject*: Using MEASURE-INDUCT*From*: Darryl Scott Dieckman <ddieckma@ececs.uc.edu>*Date*: Tue, 28 Apr 1998 17:31:27 -0400 (EDT)

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

- Prev by Date:
**Re: LOST PROOF FILES** - Next by Date:
**Re: Using MEASURE-INDUCT** - Prev by thread:
**latex problem** - Next by thread:
**Re: Using MEASURE-INDUCT** - Index(es):