On Friday, June 3, 2016 at 10:23:49 AM UTC+3, Stephan Merz wrote:
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
Oh, of course. Thanks.
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).
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.
Yeah, I know, I just wanted to see if a hybrid approach is possible (I know it's not what you'd do or want to do in TLA+, but just to test the limits of the logic), i.e. to introduce a machine only for the theorem, and keep the spec algebraic, as that is what FL was asking about.
Ron