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