Generating Correct Programs from Logic Specifications.

摘要

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)