Constructive Relational Programming: A Declarative Approach to Program Correctness and High Level Optimization,
Abstract
Program efficiency and program correctness are often conflicting aims. The efficient program may be unreadable and the well structured, obviously correct program may have unnecessary steps. We offer an approach for attaining both correctness and efficiency. Our solution includes a binary rewriting language based on Tarski and Givant's system of relation combinators. In this language smaller, correct programs can be straightforwardly combined to give larger programs. Programs can often be proved semantically equivalent using the equations of relation algebras, to give a reliable optimization method. We illustrate the expressiveness of this system by applying it to a simplified version of the stable marriages problem. We also illustrate a natural application of non-monotonic logic in which a program query accepts a database as a parameter, constructed from a complex expression. This is a new style of program construction based on a traditional, mathematical notation.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1992
- Accession Number
- ADP006612
Entities
People
- Paul Broome
Organizations
- Ballistic Research Laboratory