I checked Spivey (Understanding Z) and Woodcock (Using Z) on the conventions they use for initial state.

Neither of them uses an operation for initial state. In Spivey initial state is simply a constraint on state. In Woodcock initial state is a constraint on state'. I have no idea why Woodcock uses state', it seems to me a harmless eccentricity (but possibly this has become the norm). I observe that though one might specify intial state using an operation which puts the system into that initial state, you are then specifying a transition from some state before the initial state, and of course there aren't supposed to be any states before the initial state, so its an odd thing to do. On this basis I come to the following conclusions. Firstly, jon is out of line with both Spivey and Woodcock in using an operation to specify the initial state. To fall in line he should change Button_Init by removing the delta in the signature. That would suffice to bring him in line with Spivey. To fall in with Woodcock he would also have to add 2 primes one to Button_State and one to pushed. In neither case is Button_Init an operation, and therefore in neither case would a proof of precondition be appropriate. A consistency proof might be thought desirable. In that case the conjecture to be proven would be: exists Button_Init s.t. true On the matter of the other schemas for which jon has done precondition proofs, though a precondition proof is meaningless for a schema which is not an operation, a proof of non-emptyness (essentially a consistency proof for the predicate) might be thought worthwhile. The conjecture to be proven in that case would be the same as the one above for Button_Init. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com