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

Reply via email to