Controlled Automation of Consistency Enforcement




Consistency enforcement is an alternative to 
consistency verification. It aims at systematically modifying 
a program specification such that the result 
is consistent with respect to the specified 
set of invariants. Our approach requires the 
modified program specification to be a maximal 
consistent diminution of the original one with 
respect to some partial order. The key 
question is to find the most suitable 
partial order. There exist several justifiable choices 
for the partial order. One choice is 
operational specialization which leads to the greatest 
consistent specialization (GCS). Since operational specialization is 
equivalent to the preservation of a set 
of transition invariants, another choice arises from 
a slight modification of this set, in 
which case we talk of a maximal 
consistent effect preserver (MCE). A third choice 
would be to mix GCSs and MCEs. 
Both for GCSs and MCEs we have 
a {commutativity result: Consistency enforcement for a 
set of invariants can be done sequentially 
for an arbitrary ordering of the invariants. 
Furthermore, there is a compositionality result: Given 
the GCSs (or MCEs) of simple assignments, 
the GCSs (or MCEs) of complex program 
specifications are obtainable almost automatically by syntactic 
replacement and the computation of a precondition. 
These results enable a library-based approach to 
consistency enforcement. The selection of program specifications 
in the library defines a pragmatic enforcement 
strategy and thus sets up a controlled 
form of automation.