Design-driven compilation

Abstract

This paper introduces design-driven compilation, an ap- proach in which the compiler uses design information to drive its analysis and verify that the program conforms to its design. Although this ap- proach requires the programmer to specify additional design information, it offiers a range of benefits, including guaranteed fidelity to the designer's expectations of the code, early and automatic detection of design non- conformance bugs, and support for local analysis, separate compilation, and libraries. It can also simplify the compiler and improve its efficiency. The key to the success of our approach is to combine high-level design speciffications with powerful static analysis algorithms that handle the low-level details of verifying the design information.