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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
