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.


Proofpower mailing list

Reply via email to