Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-18T04:13:58.889Z Has data issue: false hasContentIssue false
  • English
  • Français

Logic + control: On program construction and verification

Published online by Cambridge University Press:  19 June 2017

WŁODZIMIERZ DRABENT
WŁODZIMIERZ DRABENT*
Affiliation:
Institute of Computer Science, Polish Academy of Sciences, Warsaw IDA, Linköping University, Linköping, Sweden (e-mails: [email protected])
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

logic programmingdeclarative programmingprogram completenessprogram correctnessspecificationprogram transformationflounderingoccur-check
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 18 , Issue 1 , January 2018 , pp. 1 - 29
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Apt, K. R. 1997. From Logic Programming to Prolog. International Series in Computer Science. Prentice-Hall.Google Scholar
Apt, K. R. and Luitjes, I. 1995. Verification of logic programs with delay declarations. In Proc. of Algebraic Methodology and Software Technology, AMAST '95, Alagar, V. S. and Nivat, M., Eds. Lecture Notes in Computer Science, vol. 936. Springer, 66–90.Google Scholar
Apt, K. R. and Pedreschi, D. 1993. Reasoning about termination of pure Prolog programs. Information and Computation 106, 1, 109–157.CrossRefGoogle Scholar
Bezem, M. 1993. Strong termination of logic programs. Journal of Logic Programming 15, 1&2, 79–97.Google Scholar
Carlsson, M. and Mildner, P. 2012. SICStus Prolog – the first 25 years. TPLP 12, 1–2, 35–66.Google Scholar
Clark, K. L. 1979. Predicate Logic as Computational Formalism. Technical Report 79/59, Imperial College, London. December.Google Scholar
Davis, M., Logemann, G. and Loveland, D. W. 1962. A machine program for theorem-proving. Communications of the ACM 5, 7, 394–397.CrossRefGoogle Scholar
Deransart, P. 1993. Proof methods of declarative properties of definite programs. Theoretical Computer Science 118, 2, 99–166.Google Scholar
Deransart, P. and Małuszyński, J. 1993. A Grammatical View of Logic Programming. The MIT Press.Google Scholar
Deville, Y. 1990. Logic Programming: Systematic Program Development. Addison-Wesley.Google Scholar
Drabent, W. 2012. Logic + control: An example. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12), Dovier, A. and Costa, V. S., Eds. Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, Saarbrücken/Wadern, Germany, vol. 17, 301–311. http://drops.dagstuhl.de/opus/volltexte/2012/3631.Google Scholar
Drabent, W. 2015. On completeness of logic programs. In Logic Based Program Synthesis and Transformation, LOPSTR 2014. Revised Selected Papers. Lecture Notes in Computer Science, vol. 8981. Springer. Extended version in CoRR abs/1411.3015 (2014). http://arxiv.org/abs/1411.3015.Google Scholar
Drabent, W. 2016a. Correctness and completeness of logic programs. ACM Transactions on Computational Logic 17, 3, 18:1–18:32.Google Scholar
Drabent, W. 2016b. On definite program answers and least Herbrand models. TPLP 16, 4, 498–508.Google Scholar
Drabent, W. 2017. Proving completeness of logic programs with the cut. Formal Aspects of Computing 29, 1, 155–172.Google Scholar
Drabent, W. and Miłkowska, M. 2005. Proving correctness and completeness of normal programs – a declarative approach. TPLP 5, 6, 669–711.Google Scholar
Genaim, S. and King, A. 2008. Inferring non-suspension conditions for logic programs with dynamic scheduling. ACM Transactions on Computational Logic 9, 3, 17:1–17:43.Google Scholar
Gomes, C. P., Kautz, H., Sabharwal, A. and Selman, B. 2008. Satisfiability solvers. In Handbook of Knowledge Representation, van Harmelen, F., Lifschitz, V. and Porter, B., Eds. Chapter 2, Elsevier, 89–134.Google Scholar
Howe, J. M. and King, A. 2012. A pearl on SAT and SMT solving in Prolog. Theoretical Computer Science 435, 43–55.Google Scholar
King, A. 2012. Private communication.Google Scholar
Kowalski, R. A. 1979. Algorithm = logic + control. Communications of the ACM 22, 7, 424–436.Google Scholar
Maher, M. J. 1988. Equivalences of logic programs. In Foundations of Deductive Databases and Logic Programming, Minker, J., Ed. Morgan Kaufmann, 627–658.Google Scholar
Nguyen, M. T., Schreye, D. D., Giesl, J. and Schneider-Kamp, P. 2011. Polytool: Polynomial interpretations as a basis for termination analysis of logic programs. TPLP 11, 1, 33–63.Google Scholar
Pedreschi, D. and Ruggieri, S. 1999. Verification of logic programs. Journal of Logic Programming 39, 1–3, 125–176.Google Scholar
Pedreschi, D., Ruggieri, S. and Smaus, J.-G. 2002. Classes of terminating logic programs. TPLP 2, 3, 369–418.Google Scholar
Pettorossi, A., Proietti, M. and Senni, V. 2010. The transformational approach to program development. In A 25-Year Perspective on Logic Programming: Achievements of the Italian Association for Logic Programming, GULP, Dovier, A. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 6125. Springer, 112–135.Google Scholar
Pfenning, F., Ed. 1992. Types in Logic Programming. The MIT Press.Google Scholar
Shapiro, E. 1983. Algorithmic Program Debugging. The MIT Press.Google Scholar
Smaus, J., Hill, P. M. and King, A. 1998a. Preventing instantiation errors and loops for logic programs with multiple modes using block declarations. In Proc. of Logic Programming Synthesis and Transformation, LOPSTR'98, Flener, P., Ed. Lecture Notes in Computer Science, vol. 1559. Springer, 289–307.Google Scholar
Smaus, J., Hill, P. M. and King, A. 1998b. Termination of logic programs with block declarations running in several modes. In Proc. of Principles of Declarative Programming, PLILP'98, Palamidessi, C., Glaser, H. and Meinke, K., Eds. Lecture Notes in Computer Science, vol. 1490, 73–88.Google Scholar