HOARE LOGIC, EXECUTABLE SPECIFICATIONS, AND LOGIC PROGRAMS

From Hoare correctness formulae {P} S {Q} which define first-order predicates S by their preconditions and postconditions P and Q, we formulate logic specifications S <--> P AND Q for the predicates. Subsequently, we discuss two methods to construct logic programs from logic specifications. First, we simply derive programs as the if-halves of their logic specifications. These programs are concise and readable, but often inefficient, and should rather be considered executable specifications. In the second method, we derive more efficient programs by structural induction. These programs are recursive, and-though correct-not obviously logical consequences of the preconditions and postconditions of the predicate.