Re: [tlaplus] pvs, temporal logic and stacks

[fl <freder...@xxxxxxxxxxx>]

Now, coming back to the original discussion, the question remains how you would actually prove theorem PP. Obviously, you need some form of induction, intuitively relying on an invariant saying that n equals the length of the sequence of elements that the stack contains above the element that you pushed initially, and that no execution satisfying Spec ever touches the initial part of the stack. But since S is kept abstract, there is no way of talking about that length or that part of the stack directly.

Except that you can count the number of "push" and the number of "pop" 
as it was done in Ron's specification. That way you don't need to refer to the model.
And it is the interesting part of the exercise since it involves that
you may need to use the intriguing operators of the linear temporal logic to formalize it: next, globally,
eventually, until.

For instance if you try to formalize

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

I think you need to use the operator "next"

> if you push x in the first state, and pop in the "next" one and use "top" in the "next" one you get the
> value used in the first one.

Other theorems implying that we use temporal operators can be imagined. It is of interest otherwise
temporal operators are never used. Only axiomatic specifications make them reappear.

--
FL