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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 3 Jun 2016 02:24:11 -0700 (PDT)*References*: <82bc09bd-c5b9-4d2e-86d9-bfe4e86e4083@googlegroups.com> <cb211369-98e3-47a9-88e2-d99e63700f1b@googlegroups.com> <c93fcbd9-0b5a-4d2d-8594-d5f2be40d48d@googlegroups.com> <154DA5E2-B0B1-42FF-B9AC-249F0C53FFA3@gmail.com>

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

**References**:**pvs, temporal logic and stacks***From:*fl

**Re: pvs, temporal logic and stacks***From:*Leslie Lamport

**Re: pvs, temporal logic and stacks***From:*Ron Pressler

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] pvs, temporal logic and stacks** - Next by Date:
**Re: [tlaplus] pvs, temporal logic and stacks** - Previous by thread:
**Re: [tlaplus] pvs, temporal logic and stacks** - Next by thread:
**Re: pvs, temporal logic and stacks** - Index(es):