Mechanization of an oracle in a debugging system
Anneli Edman, Sten-Ake Tirnlund · International Joint Conference on Artificial Intelligence · 1983
We shall make use of a programming calculus to derive the correct result a program is expected to compute. In this way, the decision by an oracle whether or not a result is correct can be derived formally from a specification (model) of the program, and thus the oracle can be mechanized. The debugging system consists mainly of a derivation editor and a fault finding program that collects an erroneous procedure.