Mechanization of an Oracle in a Debugging System

1. Introduction

The problem or correcting programs has troubled computer sci­ entists since the very first computer programs. Studies or the debug­ ging process itself have, for example, led to a theory or skill acquisition (Sussman, I975) and to inferring theories (Shapiro, 198I). We shall take up the debugging problem from what seems to be a new point or view, namely a verified test that can lead to a mechanized oracle.

Let us first briefly take up the relations between formal deriv:r tions, verification and formal tests or programs before we go into details or the latter idea. The situation, especially for logic programs (Kowalski, I974) is currently changing its character entirely. The ad­ vent or derivation editors (Eriksson, Johansson and Tarn lund, I 982) makes it possible to semi-automatically and formally derive correct non-trivial programs from their specifications, for example, deriva­ tions or the programs in (Hogger, I979) and (Hansson and Tarn lund, 1979) and in (Clark and Darlington, 1980) are reported in (Blomberg, Carlsson and Eriksson, I982) and (Johansson, 1983). They also re­ port on semi-automatical formal proofs or correctness or non-trivial programs, for example, the programs in (Clark and Tarnlund, I977).

The idea or deriving a program from a speciHcation is to con­ struct a correct program. In contrast, the idea or verifying that a program is correct requires that the program is constructed by an oracle. When it is correct we intend to confirm this fact , but when it is not we have, eventually, to ask an oracle for another program to verify . However, when debugging a program we know that we can not confirm that. a program is correct even after arbitrarily many tests, but still worse even a single test is not veriHed correct, since it has to rely on a judgment by an oracle i.e., an oracle decides whether or not a computed result is correct. It is this judgment that we shall formalize so the answer can be proved correct and furthermore lead to a mechanization or the oracle.

In order to carry out this idea we shall make use of a specification (model I') or a program, 1/t, in particular, a sub-specification (sub­ model 8 ~ I') that exactly speciHes a particular program. We shall use a derivation edit.or to derive an object w corresponding to an input object 1 from the sub-specification 8 that a program 1/t is supposed to compute i.e.,

2. Specifications of a class of programs and sub-specifications for a particular program

Some of the main advantages or a specification, I', are its ab­ stractness, clearness and shortness, as a consequence we often not only specify one program, 1/t , but a class[] or programs 1/t i.e.,

This is fine both when we develop programs formally and verify correctness or programs, but not so good when we want to compute, from the specification, objects that a particular program should com­ pute. For example, it could happen that we derive the input-output pair '"f,W or a predicate 1/J i.e., J'('"f,w) f- 1/J('"f,w) , but that we could not derive this pair from the program 1/t i.e., 0/l('"f,w) ~ 1/J('"f,w). What we want to find is a sub-specification 8 ~I' such that a derivation or the objects 7', w' from the sub-specification 8 i.e., 8('1',w') f- 1/J('"f',w') necessarily implies that there exists a derivation or these objects from the program 0/1 i.e., 0/1('1', w') f- 1/J('"f', w').

Let us now explain the situation more generally. Suppose that we have a specification I' and a set [] or programs as in (2) and a program 0/1 E !l that we shall test , then we want to find a specifica­ tion 8 , fr om which we can derive exactly the objects that 0/1 should compute. A sufficent condition is to find a relation, L\, that gives a sub-specification 8 i.e.,

such that the program, 1/1 , is the only element in the set

The relation, L\ , must satisfy the condition,

The relation L\ eliminates E of I' from e and can in this way, as we shall see below, shorten the computation of objects from 8 c I' in comparison to a derivation from r.

3. Deriving objects from a specification of a particular pro­ gram

Suppose that we have a specification or an insert relation I', then according to the relations (3) and (4) we want to find a condition L\ leading to a sub-specification 8 of our logic program 0/1 for inserting a label into an ordered binary tree (ob-tree). Let us now write down these expressions, in more detail in English followed by a formaliza­ tion.

where,

hence, We h:we first t he specifi cation, r, of an insert relationsh ip be­ tween two ordered binary trees (ob-tree) and a label. The ob-tree w' is the result of inserting the label u to the ob-tree w if and only if ~ II elements t hat belong to w' also belong to w or is the label u, and moreover w and w' are both ob-trees and u a label. We write this formally as:

A label u belongs to an ob-tree w if and only if u is a label and w an ob-tree constructed as t( z , y , z) and u is the label 11 or u belongs to the ob-tree z or u belongs to the ob-tree z. Formally,

An ob- tree w is either empty ,</> , or construct.ed t(z, 11, z) where both z and z are ob-trees and 11 a label, moreover, all elements that belong to z are Jess t han or equal to 11 and all elements that belong t-o z are greater than II· Formally,

A tree is either empty or const ructed of subtrees and a label.

Now all ob-trees are t rees (but not conversely)-

All constructed trees are different from the empty tre~.

However , the set r of programs is not unique, so we need a sub­ specification e (see (7)) t hat characterizes our particular program 1/t. We introduce the following condition as our .1 (see (5))

which sat isfi es .1 f- E , where E is (9), and leads to the following sub-specification e of our program 1/t

Let us write down three statements that comprise our program, 1/f .

The result of inserting a label u into an ob-tree t(z, y, z) is t(z', y, z) ir !t is less than or equal to 11 and z' is the resulting ob-tree from inserting u into the ob-tree z .

There is a symmetrical case when the b.bel u is greater than II·

So, we can now derive from our sub-specification e objects that our program 1/t shall compute. In contrast, we notice that from the specificat ion r we can derive objects that t/1 should not compute.

·· Example

The result of deriving a formula , 3w insert(t(t(</>, 5, </>), 9, </>) , 7, w) from the speci!ication, e gives the result that w is the ordered binary tree, t(t(</>, 5,t(</>, 7,</>)),9, </>) . For reasons of space, we show in the appendix the maio structure of the derivation carried out in NATDED (Eriksson, Johansson and Tarnlund, 1 982).

5. Conclusions

We have described the essential part of a debugging system whkb is b:1sed on the the programming calculus of (Hansson and Tarn lund , 1979). We use the derivation editor to compute elements of the input output pair and then ask the program to compute the same result, or conversely verify by the editor the pairs computed by the program. This leads to a formal treatment of testing, and moreover the dceision by an oracle whether or not a resu It is correct is substituted by a (semi)mechanized oracle. When a program does not compute a correct result a fault finding system selects the procedure that is responsible for the wrong instantiation. An oracle is then supposed to produce a better procedure and we can restart the testing cycle. Mechanization of the latter oracle is a goal of formal program development.

The programs we are debugging are logic programs. The system is programmed in Prolog (Colmerauer, Kanoui , Pas~ro and Roussel, 1973) and running on DEC TOPS-20 Prolog (Warren, Pereira and Perei ra, 1979).

G. Acknowledgement

The hospitality , when writing a first version of this paper , from Nils Nilsson and SRI is much appreciated. We also thank our col­ leagues at UPMAIL, in particular, Gunnar Blomberg and Martin Ni ls-­ son for their help with typesetting this paper using TE:;X.

7. References

• III Blomberg G., Carlsson M., and Eriksson L-It, De riving Logic Program·, SAIS-82, Uppsala 1982.
• 121 Clark K., and Tarnlund S-A., A Firll Order Theory of Data and Program·, IFIP-77, Toronto, North-Holland, 1V77.
• 131 Clark K., and Darlington J., Algorithm Cla11ijication Throagh S11nthe1i1, The Computer Journal 23 no 1, 1980.
• 141 Colmerauer A., Kanoui H., Pasero R., and Roussel P., Un S111ttme de Commanication Homme-mach.ine en Francai·, Re­ search Report , Groupe Intelligence Artiflcielle, Uoiversite Aix­ Marseille II, 1973.
• lSI Eriksson A., Johansson A-L., and Tarnlund S-A., Toward· a DeriMtion Editor, First International Logic Programming Con­ ference, Marseille, l 982.
• 161 Hansson A., and Tarnlund S-A., A NatartJI Programming CtJI­ ctda·, IJCAI-79, Tokyo, 1979.
• 171 Hansson A., and Tarnlund s-A., Derif!ation· in a NaturtJI Pro­ gramming CtJictdu, Electrotechnical Laboratoy Tokyo, 1979.
• lSI Hogger C., Deriflation of Logic Programm1, Ph.D. Thesis De­ partment or Computing, Imperial College, London, Hl79.
• 191 Johansson A-L. , Renlt· of Program Deriflation· in a DeriMtion Editor- NATDED, UPMAIL Report, Computing Science Depart,.. ment, Uppsala University, lV83.
• 1101 Kowalski R., Predicate Logic a1 a Programming Langaage, IFIP74, Stockholm, North-Holland, 1974.
• 1111 Shapiro E., An Algorithm th.at Infer· Theorie1 from Fact1, IJCAI-81, Vancouver, 1981.
• 1121 Sussman G., A Compater Model of Skill Acgai1ition, American Elsevier, 1975.
• 1131 Warren D., Pereira F., and Pereira L., Uur'· Gaide to Dec111ilem-10 Prolog, Department of Arti!iciallntelligence, Uni­ versity of Edinburgh, 1 V7V.

Appendix

SPECIFICATIONS VwVuVw'(insert(w, u, w') +-+ obt ree(w) A obtree(w') A label(u) A s(w, u, w')) Vw(obtree(w) .... w = ¢ V 3x3113z(w = t(x , 11. z) A obtree(x) A obtree(z) A label(ll) A Vu(uE x-+ u:::::; II) A Vu(uE z-+ u > 11)}) Vx label(x) VwVuVw'(s(w, u, w') ..... tree(w) A tree(w') A label(u) A (w =¢A w' = t(¢, u, ¢) V 3x3113z3x'311'3z'(w = t(x, 11, z) A w' = t(x', 1/, z') A 11 = 11' A (x = x' A s(z, u, z') V z = z' A s(.z, u, .z'))))) Vw(trec(w) .... w = ,PV 3x3113z(w = t(x, 11. z) A tree(.z) A tree(z) A label(11))) Vw(obtree(w)-+ tree(w)) VxV11Vz(~t(x , 11. z) = ¢) VuVw(u E w ..... label(u) A tree(w) A 3x3113z(w = t(x , 11, z) A (u = 11 VuE x VuE z))) Vu(~u E ¢) V.zV11VzVx'VII'Vz'(f(.z, 11, z) = f(x', 1/, z') -+ x' = x A 11' = 11 A z' = z) DERIVATION tree(¢) tree( I(¢, 7, ¢)) t(¢, 5, t(¢, 7, ¢)) = t(¢, 5, t(¢, 7, 4>))" tree(¢) A tree( I(¢, 7, ¢))A label(5) t(¢, 5, t(¢, 7, ¢)) = ¢ V 3x3113z(t(¢, 5, t(¢, 7, 4>)) = t(x, 11, z) A tree(x) A tree(z) A label(ll)) tree(t(¢, 5, t(¢, 7, ¢))) +-+ t(¢, 5, 1(4>, 7, ¢)) = 4> V 3x3113z(t(¢, 5, t(¢, 7, ¢)) = t(x, 11, z) A tree(x) A tree(z) A label(ll)) tree(t(¢, 5, t(¢, 7, </>))) tree(t(t(¢, 5,1(¢, 7, ¢)), II,¢)) obtree(¢) obtree(t(¢, 5, ¢)) obtree(t(t(¢, 5, ¢),II, ¢)) obtree(t(¢, 7, ¢)) Vu(u E;-+ u:::::; 5) u E t(¢, 7, ¢) 3x::iy3z(t(¢, 7, ¢) = t(x, 11. z) A (u = 11 VuE x VuE z)) ,-t(¢, 7, ¢) == t(x , 11, z)A (u =11V u E .zV u E z) u~7VuE¢VuE¢

ru = 7 r~u > 5 I :7 > 5 u>5 u=7 - u>5 ~->5 __ u> 5 u E t(¢, 7, ¢)-+ u > 5 Vu(u E t(¢, 7, ¢)-+ u > 5) t(¢, s. t(¢, 7, ¢)) = t(¢, 5, t(¢, 7, ¢))" obtree(¢) A obtree(t(¢, 7, ¢))A label(5) A Vu(u E ¢)-+ u:::::; 5) A Vu(u E t(¢, 7, ¢))-+ u > 5) t(¢, 5, t(¢, 7, ¢)) = ¢ v 3x3113z(t(¢, 5, t(¢, 7, ¢)) = t(x, II· z) A obtree(x) A obtree(z) A label(11) A Vu(u E z)-+ u:::::; II) A Vu(u E z)-+ u > 11)) obtree(t(,P, 5, t( ¢, 7, ¢))) obtrec(t(t(¢, 5, t(,P, 7, ¢)), 9, ¢)) ¢ = ¢At(¢, 7, ¢) = t(¢, 7, ¢) ¢=¢At(¢, 7, ¢) = t(¢, 7, </>) V 3z3y3z3zt311'3z'(¢ = t(x, II· z)" t(¢, 7, ¢) = t(z', II' , z')" 11 = 11' A (z = x' A s(z, 7, z') v z = z' A s(x, 7, x'))) tree(¢) A tre"(t(¢, 7, ¢))A label(7) A (¢ = 4> "t(¢, 7, ¢) = t(¢, 7,¢) v 3z3113z3z'311'3z'(¢ = t(z , 11, z) At(¢, 7, ¢) = t(z', 1/, z') A 11 = 11' A (.z = x' A s(z, 7, z') v z = z' A s(z , 7, z')))) s(¢, 7, t(¢, 7, ¢)) ..... t ree(¢) A tree(t(¢, 7, ¢))A label(7) A (¢ = ¢ "t(,P, 7, ¢) = t(¢, 7, ¢) v 3z3113z3z'311'3z'(¢ = t(z , 11, z) At(¢, 7, ¢) = t(x', 1/, z') A 11 = 11' A (x = x' A s(z, 7, z') v z = z' A s(z, 7, .z')))) s(¢, 7, t(¢, 7, ¢)) t(¢, 5, ¢) = t(¢, 5, ¢)" t(,P, 5, t(¢, 7, ¢)) = t(¢, 5, t(¢, 7, ¢))" 5 = 5 A(¢=¢ As(¢, 7, t(¢, 7, ¢)) V ¢ = t(¢, 7, </>)A s(,P, 7, ¢)) 3z3113z3z'3JI'3z'(t(¢, 5, .P) = t(z , y, z) A t(¢, 5, t(¢, 7, .P)) = t(z', 11', z') A 11 =II A (.z = z' A s(z , 7, z') V z = z' A s(z, 7, z'))) obtrce(t(¢, 5, ¢))-+tree( I(¢, 5, .P)) tree( I(¢, 5, 4>)) trec(t(¢, 5, ¢))A tree(t(¢, 5, t(¢, 7, ¢)))A label(7) A (t(¢, 5, 4>) = ¢" t(¢, 5, t(¢, 7, ¢)) = t(¢, 7, 4>) v 3z3113z3z'311'3z'(t(,P, 5, ¢) = t(x, 11 , z) A t(¢, .), t(¢, 7, ¢)) = t(x', 11', z') A II= 11' A (z = z' A s(z, 7, z') V z = z' A s(z, 7, z')))) s(t( ¢ , 5, .P ), 7, t( ¢, 5, t( 4>, 7, ¢))) s(t(t(¢, 5, ¢), II , ¢), 7, t(t(¢, 5, t(¢, 7, ¢)),11, ¢)) obtree(t(t(¢, 5, ¢), 9, ¢))A obtree(t(t(¢, 5, t(¢, 7, ¢)), 9, ¢))A label(7) A s(t(t( ¢ , 5, 4> ), II, ¢), 7, t(t( ¢, 5, t( ¢, 7, ¢)), 11 , 4>)) insert(t(t( ¢, 5, ¢), 9, 4> ), 7, t(t( ¢, 5, t(¢, 7, ¢)), 9, ¢)) .... obtree(t(t(¢, 5, ¢), 9, </>))A obtree(t(t(¢, 5, t(¢, 7, ¢)), 9, ¢))A labe1(7) A s(t(t( ¢ , 5, ¢), 9, ¢), 7, t(t(¢, 5, t( ¢, 7, ¢)), 9, ¢)) insert(t(t(¢, 5, ¢), 9, ¢), 7, t(t(¢, 5, t(¢, 7, ¢)), II, ;))