[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 PushPopTHEOREM     \A s1 \in S, x \in X : \EE s, n : PP(s1, x, s, n)!PPthis 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)!PPbut 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 asInv == /\ 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 => []InvThe 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, writingSpec == \EE s,n : SpecNow, 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,StephanOn 02 Jun 2016, at 22:43, Ron Pressler 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)          push,          pop,          top\* Algebraic structureASSUME /\ push \in [S \X X -> S]        /\ pop \in [S -> S]       /\ top \in [S -> X]\* Algebraic axiomsASSUME \A x \in X, s \in S :          /\ top[push[<>]] = x         /\ pop[push[<>]] = s------------------------------------------ MODULE PushPop ------------------------------------------EXTENDS NaturalsCONSTANTS S1, x \* initial stack and "x"ASSUME S1 \in S /\ x \in XVARIABLES s, nInit == /\ s = push[<>]         /\ n = 0        Next == \/ n' = n + 1 /\ \E y \in X : s' = push[<>]        \/ n > 0 /\ n' = n - 1 /\ s' = pop[s]Spec == Init /\ [][Next]_<>THEOREM PP == Spec => [](n = 0 => top[s] = x)====================================================================================================PP(S1, x, s, n) == INSTANCE PushPopTHEOREM     \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.