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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
