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

Re: [tlaplus] pvs, temporal logic and stacks

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, writing

Spec == \EE s,n : Spec

Now, 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.