  This paper presents an example of formal reasoning about the semantics of a
Prolog program of practical importance (the SAT solver of Howe and King). The
program is treated as a definite clause logic program with added control. The
logic program is constructed by means of stepwise refinement, hand in hand with
its correctness and completeness proofs. The proofs are declarative - they do
not refer to any operational semantics. Each step of the logic program
construction follows a systematic approach to constructing programs which are
provably correct and complete. We also prove that correctness and completeness
of the logic program is preserved in the final Prolog program. Additionally, we
prove termination, occur-check freedom and non-floundering.
  Our example shows how dealing with "logic" and with "control" can be
separated. Most of the proofs can be done at the "logic" level, abstracting
from any operational semantics.
  The example employs approximate specifications; they are crucial in
simplifying reasoning about logic programs. It also shows that the paradigm of
semantics-preserving program transformations may be not sufficient. We suggest
considering transformations which preserve correctness and completeness with
respect to an approximate specification.
