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

Re: [tlaplus] pvs, temporal logic and stacks

Hi Ron,

PP(S1, x, s, n) == INSTANCE PushPop
    \A s1 \in S, x \in X : \EE s, n : PP(s1, x, s, n)!PP

this is not what you want, and in fact, that theorem doesn't mean much: PP(...)!PP is an implication, so for it to be true it's enough to choose s and n such that PP(...)!Spec is false. For example, it is true for a variable n that is 42 initially. What you really mean is

    \A s1 \in S, x \in X : \AA s, n : PP(s1, x, s, n)!PP

but there is no need to state this theorem: it is just an instance of theorem PP in module PushPop.

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.

In "model-based" specification formalisms such as TLA+, you explicitly specify the variable s to be a sequence of X's and implement push, pop, and top using corresponding sequence operations. Then, equating S with Seq(X), the necessary invariant can be stated precisely as

Inv == /\ n \in Nat
       /\ s \in Seq(X)
       /\ Len(S) > Len(S1)
       /\ n = Len(S) - Len(S1) - 1
       /\ SubSeq(S, 1, Len(S1)+1) = Append(S1, x)

THEOREM Spec => []Inv

The proof of that theorem is a routine invariant proof, and theorem PP is an immediate consequence. No need to resort to specific "initial models".

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

Best regards,

On 02 Jun 2016, at 22:43, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

Even though TLA+ encourages machine specification (and, indeed, this works better for arbitrary data structures, and allows powerful use of refinement), I think that in this case, just for the sake of exercise, we can keep the algebraic/functional/denotational axiomatization, yet state the theorem in TLA. Perhaps like so:

------------------------------------------ MODULE Stack  ------------------------------------------
CONSTANTS X, \* The set of elements
          S, \* The set of stacks (intentionally left abstract)

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

------------------------------------------ MODULE PushPop ------------------------------------------
EXTENDS Naturals

CONSTANTS S1, x \* initial stack and "x"

ASSUME S1 \in S /\ x \in X


Init == /\ s = push[<<x, S1>>]
        /\ n = 0
Next == \/ n' = n + 1 /\ \E y \in X : s' = push[<<y, s>>]
        \/ n > 0 /\ n' = n - 1 /\ s' = pop[s]

Spec == Init /\ [][Next]_<<s, n>>

THEOREM PP == Spec => [](n = 0 => top[s] = x)

PP(S1, x, s, n) == INSTANCE PushPop
    \A s1 \in S, x \in X : \EE s, n : PP(s1, x, s, n)!PP


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.