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
