Re: [ProofPower] Initialisation convention

2012-09-23 Thread Roger Bishop Jones
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 follo

Re: [ProofPower] Initialisation convention

2012-09-23 Thread Phil Clayton
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

[ProofPower] Initialisation convention

2012-09-22 Thread Roger Bishop Jones
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 whi