LARA

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.