Generating Correct Programs from Logic Specifications.
Abstract
We have designed and implemented a system that accepts logic specifications, generates algorithms in an intermediate language, and then translates these algorithms into programs in specific target languages. The specification and intermediate languages are described in detail via their context free grammars and axiomatic semantics. It has been proved that the mappings preserve the axiomatic semantics of the programs. We discuss the system as implemented, the requirements for extending it to new target languages, and further work suggested by the project. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- May 24, 1979
- Accession Number
- ADA073023
Entities
People
- Ruth Ellen Davis
Organizations
- University of California, Santa Cruz