Re: [tlaplus] pvs, temporal logic and stacks

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

On Saturday, June 4, 2016 at 10:31:03 AM UTC+3, Stephan Merz wrote:

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.

That's true, and indeed the axioms aren't complete. I believe I understand how your axioms specify S in terms of the operations operating on it and in terms of X. Suppose we have this operator:

    RECURSIVE _ ** _
    f ** k ==
        IF k = 0 THEN [t \in DOMAIN f |-> t]
                 ELSE [t \in DOMAIN f |-> f[(f ** (k-1))[t]]]


Then your axioms are absolutely necessary to prove the theorem:

    \A s \in Stack(X) : \E n \in Nat : (pop(X) ** n)[s] = empty(X)

So I think I understand your point about the necessity for a "framework" to support algebraic reasoning (and agree that it is probably not worthwhile in TLA+).

But just for the sake of the exercise, I'm not sure that all of that is required for FL's particular theorem. More below.

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).

 Right, that was my original idea, but perhaps we can do something much simpler:
            
    Inv == top[(pop ** n)[s]] = x

where n and s are the variables in my PushPop module. I think that the invariant Inv is an inductive invariant, that it proves the theorem, and that no further axioms than "my" two (specifically with regards to the empty stack and the construction of S) are necessary to prove Inv.

Finally, while your axiomatization constructs S and its operations "from scratch" in terms of X and the axioms, wouldn't it be easier in practice to do something like the following, instead of CHOOSEing the functions etc.:

CONSTANTS X, \* The set of elements
          S, \* The set of stacks
          push, pop, top, EMPTY
         
ASSUME /\ EMPTY \in S
       /\ push \in [S \X X -> S]
       /\ pop \in [S \ {EMPTY} -> S]
       /\ top \in [S \ {EMPTY} -> X]
       /\ \A x \in X, s \in S : push[<<x, s>>] \in S \* closure
       /\ \A x \in X, s \in S : push[<<x, s>>] /= EMPTY
       /\ \A x \in X, s \in S : top[push[<<x, s>>]] = x
       /\ \A x \in X, s \in S : pop[push[<<x, s>>]] = s
       /\ \A s \in S : s = EMPTY \/ \E s1 \in S, x \in X : s = push[<<x, s1>>] 

Doesn't this specify S sufficiently in terms of X and the operations, rather than constructing S as you've done?

Ron