Towards a theory of consistency enforcement

State oriented specifications with invariants occur in almost all formal sp ecification languages. Hence the problem is to prove the consistency of the specified operations with respect to the invariants. Whilst the problem se ems to be easily solvable in predicative specifications, it usually require s sophisticated verification efforts, when specifications in the style of D ijkstra's guarded commands as e.g. in the specification language B are used . As an alternative consistency enforcement will be discussed in this paper. The basic idea is to replace inconsistent operations by new consistent ones preserving at the same time the intention of the old one. More precisely, this can be formalized by consistent spezializations, where specialization is a specific partial order on operations defined via predicate transformer s. It will be shown that greatest consistent specializations (GCSs) always exi st and are compatible with conjunctions of invariants. Then under certain m ild restrictions the general construction of such GCSs is possible. Precise ly, given the GCSs of simple basic assignments the GCS of a complex operati on results from replacing involved assignments by their GCSs and the invest igation of a guard. In general, GCS construction can be embedded in refinement calculi and ther efore strengthens the systematic development of correct programs.