A Refinement Calculus for Logic Programs
| dc.creator | Hayes, Ian | |
| dc.creator | Colvin, Robert | |
| dc.creator | Hemer, David | |
| dc.creator | Strooper, Paul | |
| dc.creator | Nickson, Ray | |
| dc.date | 2002-02-04 | |
| dc.date.accessioned | 2026-07-07T03:18:06Z | |
| dc.date.available | 2026-07-07T03:18:06Z | |
| dc.description | 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. | |
| dc.description | 36 pages, 3 figures. To be published in Theory and Practice of Logic Programming (TPLP) | |
| dc.identifier | https://arxiv.org/abs/cs/0202002 | |
| dc.identifier | http://arxiv.org/abs/cs/0202002 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/30978 | |
| dc.subject | Software Engineering | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.3.1; D.1.6 | |
| dc.title | A Refinement Calculus for Logic Programs | |
| dc.type | text |