| Thanks – I agree with almost everything you say, in particular the invariant for proving the original property via iterated function application.
On constructing the data structure vs. relying on assumptions: I think both have their place. For example, in mathematics one typically constructs, say, the real numbers via Dedekind cuts, but presents algebraic structures such as groups through characteristic axioms. For our purposes, presentation through ASSUME leaves more freedom for later implementations of the data structure later, since only the stated properties have to be satisfied – but knowing when you have stated enough properties can be difficult.
Case in point: your last conjunct
/\ \A s \in S : s = EMPTY \/ \E s1 \in S, x \in X : s = push[<<x, s1>>]
(trivially) follows from the induction rule for S that was included in my specification, but does not imply that rule. To see this, consider a structure where S is the set of finite *and infinite* sequences over X, where EMPTY is the empty sequence, and where the operations work on the first element of the sequence. This model satisfies all of your axioms, but not the induction rule: otherwise, you'd prove that the length of all elements of S is finite since
Len(EMPTY) \in Nat and \A s \in S, x \in X : Len(x) \in Nat => Len(push[x,s]) \in Nat
but the conclusion \A s \in S : Len(s) \in Nat is not true in the model. The existence of such non-standard models can cause frustration when proofs do not go through. Personally, I tend to think about data structures in terms of intended models, so I find it easier to specify them in model-based style.
P.S.
Also, due to my lack of algebra/logic/model-theory knowledge, I don't understand why your axiom about the uniqueness of S is necessary.
See above. Anyway, I think that this exercise proves Leslie's point about the difficulty of the algebraic/axiomatic approach for engineers (like me), not to speak of the difficulty of model-checking such specifications (BTW, are there model checkers for that approach?)
Fully agreed. Tool support for algebraic specifications comes mainly in the form of proof assistants, although I believe that some animation techniques similar to Alloy are possible for restricted fragments.
Best regards, Stephan
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 ** 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]] = xwhere 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 -> S]
/\ top \in [S -> 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
--
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.
|