On systematic construction of correct logic programs
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915459410952192 |
|---|---|
| author | Drabent, Włodzimierz |
| author_facet | Drabent, Włodzimierz |
| contents | Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces all the answers required by the specifications. We also consider semi-completeness -- completeness for those queries for which the program does not diverge. This paper presents an approach to systematically construct provably correct and semi-complete logic programs, for a given specification. Normal programs are considered, under Kunen's 3-valued completion semantics (of negation as finite failure) and the well-founded semantics (of negation as possibly infinite failure). The approach is declarative, it abstracts from details of operational semantics, like e.g.\ the form of the selected literals (``procedure calls'') during the computation. The proposed method is simple, and can be used (maybe informally) in actual everyday programming. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_16782 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On systematic construction of correct logic programs Drabent, Włodzimierz Logic in Computer Science Software Engineering 68N17 (Primary) 68N30, 68Q60 (Secondary) D.1.6; D.2.3; F.3.1 Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces all the answers required by the specifications. We also consider semi-completeness -- completeness for those queries for which the program does not diverge. This paper presents an approach to systematically construct provably correct and semi-complete logic programs, for a given specification. Normal programs are considered, under Kunen's 3-valued completion semantics (of negation as finite failure) and the well-founded semantics (of negation as possibly infinite failure). The approach is declarative, it abstracts from details of operational semantics, like e.g.\ the form of the selected literals (``procedure calls'') during the computation. The proposed method is simple, and can be used (maybe informally) in actual everyday programming. |
| title | On systematic construction of correct logic programs |
| topic | Logic in Computer Science Software Engineering 68N17 (Primary) 68N30, 68Q60 (Secondary) D.1.6; D.2.3; F.3.1 |
| url | https://arxiv.org/abs/2508.16782 |