Communications - September 2011

of(y). In this case, we say arrays behave in a monotone way with respect to inheritance. Using first-order axioms, we specify in Figure 3 that the inheritance relation sub(x, y) is a partial order satisfying the single inheritance property and that the array type constructor array-of(x) is monotone with respect to inheritance.

The theory of object inheritance illustrates why SMT solvers targeted at expressive program analysis benefit from general support for quantifiers.

All the applications we have treated so far also rely on a fundamental theory we have not described: the theory of equality and free functions. The axioms used for object inheritance used the binary predicate sub and the function array-of. All we know about array-of is that it is monotone over sub, and, for this reason, we say the function is free. Decision procedures for free functions are particularly important because it is often possible to reduce decision problems to queries over free functions. Given a conjunction of equalities between terms using free functions, a congruence closure algorithm can be used to represent the smallest set of implied equalities. This representation can help check if a mixture of equalities and disequalities are satisfiable, checking that the terms on both sides of each disequality are in different equivalence classes. Efficient algorithms for computing congruence closure are the subject of long-running research17 in which terms are represented as directed acyclic graphs, or

DAGS. Figure 4 outlines the operation of a congruence closure algorithm on the following limited example a = b, b = c, f(a, g(a)) ≠ f(b, g(c))

figure 4. example of congruence closure.

(a) f f

(b) f
f
g
g
g
g
a
b
c
a
b
c

(c) f f

(d) f
f
g
g
g
g
a
b
c
a
b
c

smt solvers are
a good fit for
symbolic execution
because the
semantics of
most program
statements are
easily modeled
using theories
supported by
these solvers.

In Figure 4(a), we spelled out a DAG for all terms in the example; in Figure 4(b), the equivalences a = b and b = c are represented by dashed lines; in Figure 4(c), nodes g(a) and g(c) are congruent because a = c is implied by the first two equalities; and finally, in Figure 4(d), nodes f(a, g(a)) and f(b, g(c)) are also congruent, hence the example is unsatisfiable due to the required disequality f(a, g(a)) ≠ f(b, g(c)).

Modeling. SMT solvers represent an interesting opportunity for high-level software-modeling tools. In some contexts these tools use domains from mathematics (such as algebraic data-types, arrays, sets, and maps) and have also been the subject of long-running research in the context of SMT solvers. Here, we introduce the array domain that is frequently used in software modeling.

The theory of arrays was introduced by John McCarthy in a 1962 paper28 as part of forming a broader agenda for a calculus of computation. It included two functions: read and write. The term read(a, i) produces the value of array a at index i, and the term write(a, i, v) produces an array equal to a, except for possibly index i, which maps to v. To make the terminology closer to how arrays are read in programs, we write a[i] instead of read(a, i). These properties are summarized through two equations:

write(a, i, v)[i] = v write(a, i, v)[j] = a[j] for i ≠ j

They state that the result of reading write(a, i, v) at index j is v for i = j. Reading the array at any other index produces the same value as a[j]. Consider, for example, the program swap, swapping the entries a[i] and a[j].