We define a new class of UTP homogeneous binary relations called conscriptions, which like prescriptions provide a general-correctness model of sequential computations. Their novelty is that the skip conscription is a right unit of sequential composition for all conscriptions, including even those whose assumptions refer to the after-state as well as before-state; they thus improve on prescriptions by providing a less restricted, and hence more expressive, general-correctness model for sequential computations. We also exploit our conscription concept to derive two new enriched sequential models, extended conscriptions and timed conscriptions, which differentiate between aborting and non-terminating computations.
展开▼
