Program verification

**Figure 4:** Definition of `subset/2`
$\begin{figure}\figrule \begin{verbatim}subset(L, M) :- not notsubset(L, M).n... ...rt L]). member(X, [Y\vert L]) :- member(X, L).\end{verbatim}\figrule\end{figure}$

One of the main motivations for our work is program verification and from this viewpoint it is very similar to our earlier work [NaishNaish1992b] and [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowskapear] (which contain more references related to this area). All assume that for correct programs, some atoms should succeed, some should fail and for some we don't care. The soundness and completeness results of [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowskapear] are very similar to ours, including the treatment of non-termination; the verification methods establish the same program properties. The main thing that distinguishes our current approach is the explicit use of three-valued logic. We discuss the two examples of verifying definitions of the subset relationship, where sets are represented as lists, used in [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowskapear] (and elsewhere). For the first example, given in Figure , we describe how our verification method could proceed and compare it with two other methods. For the second example we just describe our method. The intended interpretations we use for verification are chosen to be consistent with [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowskapear]. We also discuss other possible intended interpretations later. This gives some new insights into the relationship between the two examples and highlights the fact that programs can have more than one natural meaning.

With our approach to verification of Figure , we would use the following definition of admissibility: both arguments of subset/2 and notsubset/2 and the second argument of member/2 are lists. The true and false atoms should be clear from the predicate names and description above. By showing this interpretation is a model of the program, our soundness and completeness results can be established for this program.

We can show our interpretation is a model of the definition of notsubset/2, for example, by the following reasoning. If notsubset(L,M) is T, L and M are lists and there is an element of L which is not an element of M, so the body of the clause is T. If notsubset(L,M) is F, L and M are lists and there is no element of L which is not an element of M, so the body of the clause is F. The reasoning for the definition of subset/2 is trivial since the T (F) atoms of subset/2 are the F (T) atoms of notsubset/2. As well as such direct proofs we could apply the immediate consequence operators and use the propositions relating them to models.

In [NaishNaish1992b] (our first approach to dealing with inadmissibility) there are two stages to verification. The first is to show that well-typedness (admissibility) is propagated from clause heads to clause bodies. It is similar to showing that if the clause head is T or F the body is T or F (the definition is rather more complex, restricting attention to instances of negated atoms and the clause body which are true in some model). The second is to show the intended interpretation, where inadmissible atoms are considered F, is a (two-valued) model of a modified version of the program with ``type checks'' added to clause bodies (so that the body is F if the head is inadmissible). To verify notsubset/2 and subset/2, showing admissibility is propagated from heads to bodies is straightforward. Checking the interpretation is a model of the modified program is similar to the three-valued approach (though there are two extra calls in the clause bodies and instances where L or M are non-lists must be considered as well). Overall, the method is more complicated than what we now propose, and models other than the intended interpretation must be considered at one point.

In [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowskapear], two two-valued ``specifications'' are used, as discussed in Section 3.5. The ``completeness specification'' contains what we refer to as true atoms and the ``soundness specification'' contains the true and inadmissible atoms. A diagram clearly shows the three truth values we use in intended interpretations and an earlier version of the paper, [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowska2001], stated the pair of specifications ``is a formalisation of such interpretations''. Each specification is simpler than our three-valued interpretations but because two specifications are always required it is more complicated overall. There are four sets (two partitionings of the Herbrand base) instead of our three (a three-way partitioning). To support negation using this encoding of three values there is a primed (as well as original) version of each predicate, also increasing complexity. There is a priming operation on specifications and priming and double priming operations on (sets of) formulas which convert (some) atoms in the specifications/formulas into primed versions.

To verify the subset/2 definition a mixture of unions of sometimes primed specifications and sometimes primed formulas is used [Drabent and Mi $\l$ kowskaDrabent and Mi $\l$ kowska2001]. This is a very contorted way of getting at the truth table for negation in the three-valued logic, which is what our verification method uses directly. For notsubset/2 there are similar contortions but at the core of the proof there is identical reasoning to the T case in our three-valued approach. Our F case is done by showing that if the body is T or I, the head is T or I. Though slightly more complex, this may be more natural for many programmers. We feel that explicit three valued logic makes the equivalence of the two more obvious, making it easier to choose the method that seems most natural.

**Figure 5:** Alternative definition of subset, `subs/2`
$\begin{figure}\figrule \begin{verbatim}subs([], L). subs([H\vert T], LH) :- se... ... [X\vert L], [X\vert LH]) :- select(H, L, LH).\end{verbatim}\figrule\end{figure}$

Figure gives an alternative definition of the subset relationship, which can be used to generate subsets rather than only test them, so it better illustrates completeness of (terminating) all-solutions computations. Lists containing duplicates must be avoided in some places to make (finite) generation of subsets possible. Our intended interpretation is as follows (for member/2 it is the same as earlier).

For completeness we must show every true atom matches with a ground clause instance with a true body. If subs(L,LH) is T, then either L is [] (and the first clause matches) or is of the form [H|T]. If subs([H|T],LH) is T, then H is not a member of T (since it is duplicate-free), but is a member of LH, which is a list, so there exist L such that select(H,LH,L) and subs(T,L) are T. That is, there is a matching instance of the second clause with a T body.

For soundness we must show every false atom matches only with ground clause instances with false bodies. Subs([],L) cannot be F. If subs([H|T],LH) is F, then either [H|T] is not a duplicate-free list or its elements are not a subset of those in LH. That is, H is a member of T or T is not a duplicate-free list or H is not a member of LH or a member of T (other than H) is not a member of LH. That is, not member(H,T) is F or for all L, the conjunction select(H,LH,L), subs(T,L) is F.

The interesting relationship between the two subset programs can be clarified by examining other (three-valued) models of the programs. Although the success sets and the intended models we have described above are incomparable, we know both programs would be acceptable for many applications and the second program is more flexible in terms of modes (the first argument is not required to be input). One important difference between the programs is the restriction on duplicates in lists introduced. We can have a different intended interpretation of the first program where subset/2 atoms containing duplicates in the first argument are I. This interpretation is a model and the T atoms are the same as those in our intended interpretation of subs/2. The key difference between these two interpretations is that some atoms are I for subset/2 but F for subs/2.

The interpretation for subset/2 has less information ( $\subseteq_i$ ) than that for subs/2. The interpretation with less information is a model of both programs but the interpretation with more information is only a model of the program with more flexible modes. Programs which use a subset predicate only as a test can be verified using either interpretation, whereas programs which require generation of subsets need the more precise interpretation and the subset/2 definition would not be acceptable. Similarly, some programs use a subset predicate with only duplicate-free lists in the second argument. This leads to two more interpretations which are less precise but arguably more intuitive and have the same properties as the previous two. Relationships between modes and two-valued models of definite programs, and how they can be used to verify certain properties of programs, are discussed in [NaishNaish1996]. We believe three-valued models may be useful for extending this work. For example, increasing flexibility due to the existence of more models, and supporting negation.