Information Technology Reference
In-Depth Information
theorem proving is performed); the only extra input the tool might require is
some information on how to generate test data.
For example, given the function names of the standard list functions append
(++), reverse, tail, cons, empty list ([]), insert and sort, the tool produces the
following algebraic properties of the functions, fully automatically, in about 1
second:
1: insert(X,[]) = [X]
2: insert(X,[X|Xs]) = [X|[X|Xs]]
3: insert(Y,[X]) = insert(X,[Y])
4: insert(Y,insert(X,Xs)) = insert(X,insert(Y,Xs))
5: reverse([]) = []
6: reverse([X]) = [X]
7: reverse(reverse(Xs)) = Xs
8: sort([]) = []
9: sort([X|Xs]) = insert(X,sort(Xs))
10: sort(insert(X,Xs)) = insert(X,sort(Xs))
11: sort(reverse(Xs)) = sort(Xs)
12: sort(sort(Xs)) = sort(Xs)
13: sort(Ys++Xs) = sort(Xs++Ys)
14: stail([]) = []
15: stail([X|Xs]) = Xs
16: Xs++[] = Xs
17: []++Xs = Xs
18: [X|Xs]++Ys = [X|Xs++Ys]
19: reverse(Xs)++[X] = reverse([X|Xs])
20: reverse(Xs)++reverse(Ys) = reverse(Ys++Xs)
21: stail(Xs)++Xs = stail(Xs++Xs)
22: (Xs++Ys)++Zs = Xs++(Ys++Zs)
The basic method we use is the following. We start by generating a finite set
of well-typed terms that contain variables (in the above example there are 2298
such terms of depth 3). Next, we compute equivalence classes of these terms, by
means of random testing and refining: we start by assuming that all terms are
in the same equivalence class, and partition equivalence classes into smaller ones
by running random tests and inspecting the values of the terms (in the above
example, this results in 1931 equivalence classes). For each equivalence class,
we pick one representative, and produce equations between that representative
and all other terms in an equivalence class. For the example, this results in 367
equations, these are all equations that are true, but there are clearly too many
to be useful, thus we spent some effort into producing a list of non-overlapping
algebraic equations.
When one naively generates equations that hold between terms, many of which
are not independent. To reduce the number, we have developed several filtering
algorithms that remove superfluous equations. Choosing the right filtering algo-
rithm constitutes finding a balance between (1) not keeping too many equations,
