liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Logic + control: On program construction and verification
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0002-4700-7272
2017 (English)In: Theory and Practice of Logic Programming, ISSN ISSN: 1471-0684 (Print), 1475-3081 (Online)Article in journal (Refereed) Epub ahead of print
Abstract [en]

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.

Place, publisher, year, edition, pages
Cambridge University Press, 2017.
Keyword [en]
logic programming, declarative programming, program completeness, program correctness, specification, program transformation, floundering, occur-check
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:liu:diva-141146DOI: 10.1017/S1471068417000047OAI: oai:DiVA.org:liu-141146DiVA: diva2:1143910
Available from: 2017-09-23 Created: 2017-09-23 Last updated: 2017-09-26

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Drabent, Wlodzimierz
By organisation
Software and SystemsFaculty of Science & Engineering
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 7 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf