Verification of Logic Programs with Delay Declarations

Verification of Logic Programs with Delay Declarations

Abstract

Program verification has to exploit a knowledge of the program behaviour to ensure that the program executes terminates normally with correct answers. Prolog, although based on first order logic and has an implementation based on resolution, has a number of practical features that may cause a program to terminate abnormally. Moreover, most Prolog systems have some form of delay declarations (eg the Block declarations of SICStus Prolog) that allow the programmer to insist that certain atomic calls are delayed until they are sufficiently instantiated. We have considered a number of aspects of verification relevant to Prolog programs. These include occur-check freedom, flounder freedom, freedom from errors related to built-ins, and termination. The occur-check in unification procedures which avoids the generation of infinite data-structures is expensive and often omitted. Floundering means that the program stops without any useful solution and is caused when all the atoms to be executed are postponed because of the delay declarations. Arithmetic operators provided in Prolog often require the arguments to be ground and if they are not sufficiently instantiated, the program terminates with an error message. In this talk, I will describe existing techniques for verifying Prolog programs without delay declarations and then show how this work can be lifted to programs with delays such as the Block declarations of SICStus Prolog.