Re: [tlaplus] pvs, temporal logic and stacks

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. People working on algebraic specifications introduced a whole theory of initial models (and also, dually, of final models) that give you suitable inductive proof rules, and various conditions that ensure when a specification has such models.

This I don't understand. Is there no way to do the induction structurally, based on the axioms to (as you'd do in algebraic proofs)? The invariant is true in the initial condition based on the first axiom, and then you can introduce a sequence of elements (ys) for the sake of the proof, while making no further assumptions about S. So you can talk about that part of the stack as a sequence (literally) of algebraic operations (push) without exploring S (and then Len(ys) >= 0).

I understand the intention, but your axioms

\* Algebraic structure
ASSUME /\ push \in [S \X X -> S]
       /\ pop \in [S -> S]
       /\ top \in [S -> X]

\* Algebraic axioms
ASSUME \A x \in X, s \in S :
         /\ top[push[<<x, s>>]] = x
         /\ pop[push[<<x, s>>]] = s

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