Towards a theory of consistency enforcement (Q1284698)

The article discusses consistency enforcement for static invariants as an alternative to consistency verification in model-based formal specifications. 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 semantic equivalence classes of operations defined via predicate transformers. In the article it is shown that Greatest Consistent Specializations (GCSs) always exist and are compatible with conjunctions of invariants. Then under certain technical restrictions described by the notion of \({\mathcal I}\)-reducedness a compositionality result for the construction of such GCSs is achieved. Precisely, given the GCSs of simple basic assignments the GCS of a complex operation results from replacing involved assignments by their GCSs and the investigation of a guard.