Please use this identifier to cite or link to this item:
Scopus Web of Science® Altmetric
Type: Journal article
Title: A refinement calculus for logic programs
Author: Hayes, I.
Colvin, D.
Hemer, D.
Strooper, P.
Nickson, R.
Citation: Theory and Practice of Logic Programming, 2002; 2(4-5):425-460
Publisher: Cambridge University Press
Issue Date: 2002
ISSN: 1471-0684
Statement of
Ian Hayes, Robert Colvin, David Hemer, Paul Strooper And Ray Nickson
Abstract: Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and re nement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.
Keywords: refinement calculus; logic programming
Provenance: Published online by Cambridge University Press 26 Jul 2002
Rights: Copyright © 2002 Cambridge University Press
RMID: 0020064280
DOI: 10.1017/S1471068402001448
Published version:
Appears in Collections:Computer Science publications

Files in This Item:
File Description SizeFormat 
Hayes_33978.pdfPublished version260.62 kBAdobe PDFView/Open

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.