[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
eventually(p : [Queue->bool], q : Queue): RECURSIVE bool =
IF p(q) THEN
ELSIF empty?(q) THEN
The TCC's for eventually are satisfied, because value(q) will
Hopefully I have given enough information to get some help with the
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?