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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sat, 4 Jun 2016 09:31:01 +0200*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> <c782fde4-25bb-407f-8a26-34176a58f0ef@googlegroups.com>

I understand the intention, but your axioms
are not strong enough for justifying a principle of structural induction. In particular, there is no formal basis for asserting that the parameter set S is constructed by (the empty stack and) the push operation. Also, there could be other operations on stacks. It seems to me that if you want to simulate an algebraic specification of a stack in TLA+, you need to write something like StackAxioms(X,S,mt,ps,pp,tp) == /\ mt \in S /\ ps \in [S \X X -> S] /\ pp \in [S -> S] /\ tp \in [S -> X] /\ \A x \in X, s \in S : pp[ps[s,x]] = s /\ tp[ps[s,x]] = x /\ \A x \in X, s \in S : mt # ps[s,x] /\ \A T \in SUBSET S : mt \in T /\ (\A x \in X, s \in T : ps[s,x] \in T) => S = T push(X) == CHOOSE ps : \E S, mt, pp, tp : StackAxioms(X,S,mt,ps,pp,tp) Stack(X) == DOMAIN push(X) empty(X) == CHOOSE mt : \E pp, tp : StackAxioms(X, Stack(X), mt, push(X), pp, tp) pop(X) == CHOOSE pp : \E tp : StackAxioms(X, Stack(X), empty(X), push(X), pp, tp) top(X) == CHOOSE tp : StackAxioms(X, Stack(X), empty(X), push(X), pop(X), tp) In order to justify that these definitions are sensible, you first need to prove THEOREM StackExistence == \A X : \E S,mt,ps,pp,tp : StackAxioms(X,S,mt,ps,pp,tp) which is possible by exhibiting the standard model based on sequences. Then, prove similar theorems justifying the definitions involving CHOOSE. Finally, you can derive the desired induction rule THEOREM StackInduction == ASSUME NEW X, NEW P(_), P(empty(X)), \A s \in Stack(X), x \in X : P(s) => P(push(X)[s,x]) PROVE \A s \in Stack(X) : P(s) Finally, it looks like you can augment your specification with a history variable y that records the sequence of elements that have been pushed on top of the element x pushed in the initial condition but not yet popped off and prove that the stack s in the specification behaves like that sequence y (i.e., top and pop applied to s yield the same values as the analogous operations applied to y). If you want to use TLA+, the standard way of specifying a stack directly as a sequence (and possibly hiding the sequence using \EE) looks much more straightforward. Formalisms for algebraic specifications hide all this complexity in customized patterns whose correctness has been proved once and for all at the meta-level. For example, in CASL you'd write spec STACK = sorts X free type Stack ::= empty | push(Stack; X) ops top : Stack -> X pop : Stack -> Stack vars s : Stack; x : X axioms top(push(s,x)) = x pop(push(s,x)) = s end and the semantic analyzer would check that this specification is well-formed and generate the corresponding induction rule. It ought to be possible to pre-define corresponding patterns within TLA+, but it's not clear to me how often they would be useful. When it comes to more complex data structures (say, balanced trees), you tend to need more control than algebraic specifications can provide. NB: The above construction of stacks is similar to the definition of natural numbers in TLA+'s standard modules. Best regards, Stephan |

**Follow-Ups**:**Re: [tlaplus] pvs, temporal logic and stacks***From:*Ron Pressler

**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

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

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