A simple correctness proof for magic transformation

DOI10.1017/S1471068411000032zbMATH Open1255.68050OpenAlexW2134148399MaRDI QIDQ4897705FDOQ4897705

Authors Włodzimierz Drabent

Publication date 27 December 2012

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1012.2299

zbMATH Keywords

logic programmingprogram correctnessoperational semanticsdeclarative semanticsLD-resolutionmagic transformation

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Abstract: The paper presents a simple and concise proof of correctness of the magic transformation. We believe it may provide a useful example of formal reasoning about logic programs. The correctness property concerns the declarative semantics. The proof, however, refers to the operational semantics (LD-resolution) of the source programs. Its conciseness is due to applying a suitable proof method.

Recommendations

• scientific article; zbMATH DE number 1926633
• scientific article; zbMATH DE number 1534593
• Constraint-based correctness proofs for logic program transformations
• Automatic Correctness Proofs for Logic Program Transformations
• Totally correct logic program transformations via well-founded annotations

Cites work

• scientific article; zbMATH DE number 1926614 (Why is no real title available?)
• Abstract interpretation: a kind of magic
• Inductive assertion method for logic pograms
• Magic templates: a spellbinding approach to logic programs
• On the power of magic
• Proof methods of declarative properties of definite programs
• Proving correctness and completeness of normal programs – a declarative approach
• Reasoning about prolog programs: From modes through types to assertions
• The s-semantics approach: Theory and applications

Cited in

(2)

• scientific article; zbMATH DE number 3859014 (Why is no real title available?)
• scientific article; zbMATH DE number 1926633 (Why is no real title available?)

This page was built for publication: A simple correctness proof for magic transformation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4897705)