Re: [ProofPower] Initialisation convention
Phil, On Sunday 23 Sep 2012 21:11, Phil Clayton wrote: > By making initialization an operation without a before > state, the initialization can be used with schema > operators such as composition and pre, e.g. > >Init ⨟ Op > >pre Init > > the latter being another way to write the following: >∃ Init ∙ true >∃ State' ∙ Init That had occurred to me. But it didn't seem to me a particularly good idea. One could generally state the non-emptyness of some schema S as pre S', but surely its clearer to say ∃ S ∙ true. (and Init /\ Op does the same under Spivey's convention as Init ⨟ Op under the other). There doesn't seem to be much to chose between them. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Initialisation convention
On 22/09/12 10:45, Roger Bishop Jones wrote: I see that Potter Sinclair and Till "An Introduction to Formal Specification Using Z" 1991 use the primed version of the convention, and offer the following rationale (p43): "Here we use Vocab' as the variable to suggest that initialisation is like an operation which produces after objects which are acceptable as starting values for the persistent objects of the system. Admittedly in this very simple case this seems a complicated way of saying that the system must start with an empty vocabulary." (but note that they did not actually use an operation, the initial state is defined as a bare after-state). Possibly the priming of initial state began here. By making initialization an operation without a before state, the initialization can be used with schema operators such as composition and pre, e.g. Init ⨟ Op pre Init the latter being another way to write the following: ∃ Init ∙ true ∃ State' ∙ Init Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Initialisation convention
I see that Potter Sinclair and Till "An Introduction to Formal Specification Using Z" 1991 use the primed version of the convention, and offer the following rationale (p43): "Here we use Vocab' as the variable to suggest that initialisation is like an operation which produces after objects which are acceptable as starting values for the persistent objects of the system. Admittedly in this very simple case this seems a complicated way of saying that the system must start with an empty vocabulary." (but note that they did not actually use an operation, the initial state is defined as a bare after-state). Possibly the priming of initial state began here. But Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
