Program Transformation with Abstract Relation Algebras
Abstract
Our objective is to satisfy two seemingly opposing constraints on program design. We want to begin a program as an obvious formal specification but also insist upon efficient execution. Our approach is to find expressive, model independent program constructs with algebraic properties that can show logical equivalence between a clear specification and an efficient program. Our solution is an implementation of some of the relations, relation operators, and equations that comprise Tarski's Q-relation algebra. The key to this solution is a single operator for linear recursions that satisfies two equations. The first merges recursions and the second propagates constraints for early pruning of the nonproductive branches of the computation tree.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1989
- Accession Number
- ADA213270
Entities
People
- Paul Broome
Organizations
- Ballistic Research Laboratory