Verification of Logic Programs and Imperative Programs.
Lee Naish · 1991
This paper explores the relationship between verification of logic programs and imperative programs with the aim of uncovering the kinds of reasoning used to construct logic programs. We discuss forward reasoning, such as that used for verifying imperative programs using the inductive assertion method, and backward reasoning, such as that used for verifying imperative programs using subgoal induction and logic programs using consequence verification. We argue that consequence verification is often inadequate for Prolog programs because programmers make implicit assumptions about how procedures are called. These assumptions can be made explicit using general type declarations. Verification of logic programs with type declarations can be done in two steps. We show that one corresponds to subgoal induction and the other corresponds to the inductive assertion method. Thus two existing verification methods are combined. The forward and backward reasoning inherent in this method of verificat...