Towards an Arithmetic Theory of Consistency Enforcement based on Preservation of delta-constraints

Abstract

Consistency Enforcement provides an alternative theory to common verification techniques within formal specification languages. We consider specifications in the form of guarded commands. The basic idea is then to replace a program specification S by its greatest consistent specialization (GCS) S_I which is provably consistent with respect to a given static constraint I, preserves the effects of S according to a specialization order and is maximal with these properties. The theory has been shown to provide several strengths. In particular, the enforcement process for a huge class of complex specifications can be reduced to its basic components. Moreover, the result can be obtained sequentially and is independent from the order of the given constraints. In addition, arithmetic logic has been used to show that GCSs can be efficiently computed for a reasonably large class of program specifications and invariants. However, all results have been achieved with respect to the underlying specialization order. The simplicity of this order reveals some obvious weaknesses. In this paper, we show how the specialization order can be replaced by the notion of δ-constraints. Specialization of a program specification S turns out to be equivalent to the preservation of all δ-constraints on the underlying state space of S. Obviously, this enables us to weaken the specialization order towards the preservation of certain δ-constraints. We define maximal consistent effect preservers (MCEs), show that these are closely related to GCSs and prove that MCEs can be obtained sequentially and independently from the order of a given set of static constraints. This backs up the conjecture that the notion of MCEs leads towards a tailored theory of consistency enforcement.