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

# pvs, temporal logic and stacks

Having a look at PVS, ( a nice system but with no temporal logic embedded)

>  http://pvs.csl.sri.com/

and reading in their tutorials the pages where a stack is specified

>  http://www.csl.sri.com/papers/wift-tutorial/wift-tutorial.pdf  (p. 44)

I have come across axioms like

> top(push(x, s)) = x

or

> pop(push(x, s)) = s

and theorems like

>  pop(pop(push(x, push(y, s)))) = s

so far so good. But it comes to my mind that the style of theorems you really want would be better

> if you push an x and then applies any sequence of "push" and "pop" ("push" and "pop" in equla number)
> you will retrieve your x with "top".

And I think that you need a temporal logic to express (easily) this property. But I don't
exactly know which one?

So it is my question: WHICH ONE?

(To tell the truth I suppose with a sequence of "push" and "pop" we can express this theorem in PVS but
with a temporal logic it would look more natural).

--
FL