Paper Info
Title
A refinement calculus for logic programs
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 refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.
Year
DOI
Venue
2002
10.1017/S1471068402001448
TPLP
Keywords
Field
DocType
universal quantification,refinement law,wide-spectrum logic programming language,refinement calculus,correctness-preserving refinement,existing refinement,wide-spectrum language,existential quantification,declarative semantics,logic program,programming language,spectrum,software engineering,logic programming
Programming language,Situation calculus,Refinement calculus,Computer science,Proof calculus,Algorithm,Zeroth-order logic,Theoretical computer science,Refinement,Logic programming,Process calculus,Curry–Howard correspondence
Journal
Volume
Issue
ISSN
2
4-5
1471-0684
Citations 
PageRank 
References 
3
0.41
14
Authors
5
Name
Order
Citations
PageRank
Ian J. Hayes163462.03
Robert Colvin2688.67
David Hemer3192.86
Paul Strooper470168.70
Ray Nickson5575.60