Loading...
Please wait, while we are loading the content...
Similar Documents
A refinement calculus for logic programs
| Content Provider | Scilit |
|---|---|
| Author | Hayes, Ian Colvin, Robert Hemer, David Strooper, Paul Nickson, Ray |
| Copyright Year | 2002 |
| 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. |
| Related Links | https://digital.library.adelaide.edu.au/dspace/bitstream/2440/33978/1/Hayes_33978.pdf https://core.ac.uk/download/pdf/12756017.pdf https://www.cambridge.org/core/services/aop-cambridge-core/content/view/76C4148F9CCFB28D9718A33924640BCC/S1471068402001448a.pdf/div-class-title-a-refinement-calculus-for-logic-programs-div.pdf |
| Ending Page | 460 |
| Page Count | 36 |
| Starting Page | 425 |
| ISSN | 14710684 |
| e-ISSN | 14753081 |
| DOI | 10.1017/s1471068402001448 |
| Journal | Theory and Practice of Logic Programming |
| Issue Number | 4-5 |
| Volume Number | 2 |
| Language | English |
| Publisher | Cambridge University Press (CUP) |
| Publisher Date | 2002-07-01 |
| Access Restriction | Open |
| Subject Keyword | Theory and Practice of Logic Programming Hardware and Architecture History and Philosophy of Science Refinement Calculus Logic Programming |
| Content Type | Text |
| Resource Type | Article |
| Subject | Artificial Intelligence Theoretical Computer Science Computational Theory and Mathematics Hardware and Architecture Software |
