Logic + control: on program construction and verification
From MaRDI portal
Abstract: 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.
Recommendations
Cites work
- scientific article; zbMATH DE number 870438 (Why is no real title available?)
- A 25-year perspective on logic programming. Achievements of the Italian Association for Logic Programming, GULP
- A machine program for theorem-proving
- A pearl on SAT and SMT solving in Prolog
- Algebraic methodology and software technology. 4th international conference, AMAST '95, Montreal, Canada, July 3--7, 1995. Proceedings
- Algorithm = logic + control
- Classes of terminating logic programs
- Correctness and completeness of logic programs
- Inferring non-suspension conditions for logic programs with dynamic scheduling
- Logic + control: an example
- On completeness of logic programs
- On definite program answers and least Herbrand models
- Polytool: polynomial interpretations as a basis for termination analysis of logic programs
- Proof methods of declarative properties of definite programs
- Proving completeness of logic programs with the cut
- Proving correctness and completeness of normal programs – a declarative approach
- Reasoning about termination of pure Prolog programs
- SICStus Prolog -- the first 25 years
- Strong termination of logic programs
- Verification of logic programs
Cited in
(15)- Backjumping is Exception Handling
- Correctness and completeness of logic programs
- Logic control and ``reactive systems: algorithmization and programming
- Logic + control: an example
- scientific article; zbMATH DE number 3956407 (Why is no real title available?)
- Logic and Control
- On correctness of normal logic programs
- The Prolog debugger and declarative programming
- Implementing backjumping by means of exception handling
- On Correctness and Completeness of an n Queens Program
- A relaxed condition for avoiding the occur-check
- scientific article; zbMATH DE number 879006 (Why is no real title available?)
- A note on occur-check
- Controlling Program Extraction in Light Logics
- scientific article; zbMATH DE number 1531362 (Why is no real title available?)
This page was built for publication: Logic + control: on program construction and verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4603427)
