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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 3 Jun 2016 02:01:30 -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>

It is true that the specification stated like this commits to implementing the stack as a sequence, which may not be what you want. The abstract spec is easily obtained by hiding s and n, writingSpec == \EE s,n : SpecNow, you can implement the stack as you like and need only prove that it behaves as if there were a sequence s and counter n.

Yes. In many specifications engine now

> http://frama-c.com/download/acsl-implementation-Aluminium-20160501.pdf (p. 72 & 74)

they have what they call model variables or ghost variables and the formula

> Spec == \EE s,n : Spec

seems to be the exact way of translating the concept into TLAPLUS.

I believe that is essentially what Leslie meant when he wrote that the algebraic and the model-based styles of specifying a stack were isomorphic.

It looks so.

--

FL

**Follow-Ups**:

**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: 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: [tlaplus] pvs, temporal logic and stacks** - Index(es):