Hostname: page-component-78c5997874-ndw9j Total loading time: 0 Render date: 2024-11-04T19:48:37.482Z Has data issue: false hasContentIssue false
  • English
  • Français

A refinement calculus for logic programs

Published online by Cambridge University Press:  26 July 2002

IAN HAYES ,
ROBERT COLVIN ,
DAVID HEMER ,
PAUL STROOPER  and
RAY NICKSON
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
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

refinement calculuslogic programming
Type
Research Article
Information
Theory and Practice of Logic Programming , Volume 2 , Issue 4-5 , July 2002 , pp. 425 - 460
Copyright
© 2002 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)