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

(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


Proofpower mailing list

Reply via email to