An Uninterpreted Program (UP) is one where all variables and functions are uninterpreted. That is, all variables have the same type and functions do not have definitions. The following program is uninterpreted:
1
2
3
4
5
6
7
8
9
10
11
x := t;
y := t;
while (c != d) {
x := n(x);
y := n(y);
c := n(c);
}
x := f(a, x);
y := f(b, y);
assume(a == b);
assume(x != y);
The variables x, y, t, c, d, a, b are all of the same type. Since they are all the same type, we can do assignments like x := t and comparisons like a == b. Since they are uninterpreted, we cannot do any operations like addition or concatenation. Functions like n and f are also uninterpreted: they do not have definitions. The only constraint they have to satisfy is congruence: for any two variables a and b and any unary function g, if a == b then g(a) == g(b). Similarly for n-ary functions as well. The state of an UP is a mapping from program variables to terms: constants or uninterpreted functions applied to terms. Initially, all variables are mapped to special constants, denoted by capital letters. In the example, after executing line 1, the state would be [x --> T; t --> T; y --> Y; ... ]
Since UP do not have any complicated sorts or operations they are easy to understand. However, checking reachability in UP is undecidable, making them very interesting from a theoretical point of view. The authors in 1 introduced a decidable subclass of UP called Coherent UP. A UP is a CUP if, in all its executions, (a) no term is recomputed unless it is stored in a variable and (b) whenever there is an assume(a == b) statement, all computed superterms of terms stored in a and b are stored in variables. Our example program is a CUP: (a) Whenever terms are recomputed, they are stored in variables. After one iteration of the while loop, x and y store the term n(T). Then x is updated to n(n(T)). Subsequently, the term n(n(T)) is recomputed to be stored in y but it is already store in x (b) when the execution reaches assume(x == y), all superterms of x,y, (f(x, a) and f(y, b)) are stored in variables (a, b).
[1] claims that, to check reachability in CUP programs, we only need to keep track of a finite amount of information. In particular, it is enough to keep track of equalities and inequalities between program variables and equalities of the form x = f(y). We can forget the actual value assigned to variables and equalities containing nested function applications. In the while loop in our example, this amounts to keeping track of the relationship between x and y as both are updated but not the actual values of x and y (n(n(...(n(T))...))).
However, we think that this information is not enough to check reachability. The example above demonstrates it. Just before the assumption on line 10, x and y are neither equal nor unequal and are not related by function applications. However, they are both equal to f(N, A) and f(N, B), where N is a deep nested term. The assumption at line 10 makes them equal. Thus, even though x and y were not related before line 10, they are equal after the assumption.
To overcome this dilemma, it might seem like we need to keep track of exact values of the variables. But we prove that we only have to keep track of special relationships between variables. In addition to equalities, inequalities, and one level function applications, we need to keep track of implications of the form a == b ==> x == y. Since there are only finitely many such implications, CUP is still decidable. We prove that inductive invariants of CUP are of depth at most 1. More deatils can be found in our paper.