Hi Ron,PP(S1, x, s, n) == INSTANCE PushPop 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, Stephan
|