Hostname: page-component-745bb68f8f-l4dxg Total loading time: 0 Render date: 2025-02-06T00:44:31.743Z Has data issue: false hasContentIssue false

A refinement calculus for logic programs

Published online by Cambridge University Press:  26 July 2002

IAN HAYES
Affiliation:
School of Information Technology and Electrical Engineering, The University of Queensland, Australia
ROBERT COLVIN
Affiliation:
School of Information Technology and Electrical Engineering, The University of Queensland, Australia
DAVID HEMER
Affiliation:
School of Information Technology and Electrical Engineering, The University of Queensland, Australia
PAUL STROOPER
Affiliation:
School of Information Technology and Electrical Engineering, The University of Queensland, Australia
RAY NICKSON
Affiliation:
School of Mathematical and Computing Sciences, Victoria University of Wellington, New Zealand
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Copyright
© 2002 Cambridge University Press