Preventing Instantiation Errors and Loops for Logic Programs with Several Modes Using block Declarations

We present verification methods for logic programs with delay declarations, showing how type and instantiation errors related to built-ins can be avoided, and how termination can be ensured. Three features are distinctive of this work: (a) we assume that predicates can be used in several modes; (b) we show that block declarations, which are a particularly simple delay construct, are sufficient to ensure the desired properties; (c) we take the selection rule into account, assuming it to be the rule of most Prolog implementations. These methods can be used both to verify existing programs and to assist in writing new programs.