ARGUS/V: A SYSTEM FOR VERIFICATION OF PROLOG PROGRAMS.

The verification system Argus/V for proving properties of Prolog programs is outlined by contrasting verification with testing in logic programming. Specifications in Argus/V are given by a class of first-order formulas, including goals for normal execution. The specification states a partial property of the program that states what the program does as a whole. Though verification in Argus/V does not guarantee the correctness of the program at one stroke, the more properties of the program proved the closer the program is to what the authors intend. Verification in Argus/V is done using inference rules. Execution in Prolog, on which testing is based, is a special case of the inferences in the verification.