Logic programs as specifications in the inductive verification of logic programs

AbstractIn this paper we define a new verification method based on an assertion language able to express properties defined by the user through a logic program. We first apply the verification framework defined in [3] to derive sufficient inductive conditions to prove partial correctness. Then we show how the resulting conditions can be proved using program transformation techniques