[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


> 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).