Proving Invariants Containing Relations

Simplified version of the example from a quiz.

r1 = r
k = 0
W = {}
while //: W = range(r \ r1)
      (r1 != {}) {
  v1 = lookup(k,r1)
  W = W union v1
  r1 = r1 \ ({k} x v1)
}

Note that this program does not mention integers. In fact, the fact that $k$ is integer is not important for partial correctness, only for termination. However, it can be helpful to know that we could assume the first and the second components of $r$ to be disjoint.

Postcondition of v1=lookup(k,r1) implies, among others:

$\begin{equation*} \{k\} \times v1 \subseteq r1 \end{equation*}$

Indeed, this holds when $v1=\{v\}$ because then $(k,v) \in r1$ . When $v1=\{\}$ , then the condition trivially holds.

Note that the negation of $p_1 \land \ldots \land p_n \rightarrow p$ is $p_1 \land \ldots \land p_n \land \lnot p$ .

The negation of the verification condition that implies that invariant is preserved has (among others) the following conjuncts:

$W = range(r \setminus r1)$ (assume invariant)
$|v1| \le 1$ , $\{k\} \times v1 \subseteq r1$ (postcondition of lookup)
$W' = W \cup v1$ (loop body)
$r1' = r1 \setminus ({k} \times v1)$ (loop body)
$W' \neq range(r \setminus r1')$ (asserting invariant–note that VC is negated)

Now translate the operations on sets and relations into first-order logic, by introducing

unary predicates for $W,W'$
binary predicates for $r,r1,r1'$

and identifying sets and relations with the corresponding predicates.

We translate each conjunct into first-order logic.

Clause 1

$W = range(r \setminus r1)$

Note that, for all $v$ ,

$\begin{equation*} v \in range(\rho) \iff \exists i. (i,v) \in \rho \end{equation*}$

We obtain

$\begin{equation*} \forall v.\ W(v) \iff \exists i. r(i,v) \land \lnot r1(i,v) \end{equation*}$

which decomposes into implication from right to left:

$\begin{equation*} \lnot r(i,v) \lor r1(i,v) \lor W(v) \end{equation*}$

and the implication left to right:

$\begin{equation*} \forall x. \exists y.\ \lnot W(x) \lor (r(x,y) \land \lnot r1(x,y)) \end{equation*}$

that Skolemizes and decomposes into two clauses:

$\begin{equation*} \lnot W(x) \lor r(x,f(x)) \end{equation*}$

$\begin{equation*} \lnot W(x) \lor \lnot r1(x,f(x)) \end{equation*}$

Note that the Skolem function in the original problem maps indices into results of the array. If we worked in many-sorted logic, we could assume that it has type $f : A \to B$ for two incompatible types $A,B$ where $r \subseteq A \times B$ and $W \subseteq A$ . This means that expressions such as $f(f(x))$ are not meaningful and restricts Herbrand universe. See the paper Decidable fragments of many-sorted logic.

Clause 2

v1 is a set which is singleton, so we can add the axiom

$\exists a. \forall v. (v1(v) \rightarrow v=a)$

and we Skolemize $a$ . Note that we do not claim $v1(a)$ , since it could be empty.

Then

$\{k\} \times v1 \subseteq r1$ (postcondition of lookup)

becomes

$\begin{equation*} \lnot v1(v) \lor r1(k,v) \end{equation*}$

Clause 3

$W' = W \cup v1$ (loop body)

$\begin{equation*} \forall v. (W'(v) \iff (W(v) \lor v1(v))) \end{equation*}$

That is, from left to right:

$\begin{equation*} \lnot W'(v) \lor W(v) \lor v1(v) \end{equation*}$

and from right to left:

$\begin{equation*} \lnot W(v) \lor W'(v) \end{equation*}$

$\begin{equation*} \lnot v1(v) \lor W'(v) \end{equation*}$

Clause 4

$r1' = r1 \setminus ({k} \times v1)$ (loop body)

$\begin{equation*} \forall i,v. r1'(i,v) \iff (r1(i,v) \land \lnot (i=k \land v1(v))) \end{equation*}$

and this decomposes further.

Clause 5

$W' \neq range(r \setminus r1')$

$\begin{equation*} \lnot (\forall v.\ W(v) \iff \exists i. r(i,v) \land \lnot r1(i,v) \end{equation*}$

$\begin{equation*} \exists b.\ \lnot (W(b) \iff \exists i. r(i,b) \land \lnot r1(i,b)) \end{equation*}$

So we obtain another Skolem constant, b and negation of equivalence. Equivalence is false iff at least one side is true and at least one is false, so we obtain

$\begin{equation*} W(b) \lor \exists i. r(i,b) \land \lnot r1(i,b)) \end{equation*}$

$\begin{equation*} \lnot W(b) \lor \lnot (\exists i. r(i,b) \land \lnot r1(i,b))) \end{equation*}$

In the first case we obtain another Skolem constant i1 and two clauses:

$\begin{equation*} W(b) \lor r(i1,b) \end{equation*}$

$\begin{equation*} W(b) \lor \lnot r1(i,b)) \end{equation*}$

In the second case we obtain the clause:

$\begin{equation*} \lnot W(b) \lor \lnot r(i,b) \lor r1(i,b) \end{equation*}$

Summary

Variables $i,v$ are universally quantified, $a,k$ are constants, $f$ is function symbol:

$\lnot r(i,v) \lor r1(i,v) \lor W(i)$
$\lnot W(v) \lor r(f(v),v)$
$\lnot W(v) \lor \lnot r1(f(v),v)$
$\lnot v1(v) \lor v=a$
$\lnot v1(v) \lor r1(k,v)$
$\lnot W'(v) \lor W(v) \lor v1(v)$
$W'(v) \lor \lnot W(v)$
$W'(v) \lor \lnot v1(v)$
…

We obtain many, but finitely many clauses. Moreover, if we respect typing constraints, we obtain a finite Herbrand universe.

$\begin{equation*} H = \{ a, b, k, i1, f(a), f(b) \} \end{equation*}$

So we just need to instantiate the universally quantified clauses with those values (respecting types will further help). Note that we need to consider cases where $a=b$ and the cases where $a\neq b$ .

Universal Class

Whenever Herbrand model (in unsorted or many-sorted sense) is finite, Herbrand theorem gives us a decision procedure for this logic.

One such class are formulas that have no function symbols, and where existentials appear only at the top level. This is so-called “effectively propositional logic” (EPR), or the Bernays-Schoenfinkel-Ramsey class of first-order logic.

This class can encode, for example, formulas that talk about relations with set algebra operations, because those operations give either universal quantifiers or top-level existential quantifiers.