META-AMPHION: Synthesis of Efficient Domain-Specific Program Synthesis Systems

摘要

Amphion is a real-world knowledge-based software engineering (KBSE) system whose program synthesis subsystem is based on deductive synthesis. Amphion is designed to automate use of software component libraries—the programs it generates are compositions of software components. Amphion has a domain-independent generic architecture that is specialized to an application domain and component library through a declarative domain theory. Up to now, program synthesis has been made efficient and automatic through manual tuning of theorem-proving strategies and tactics, and careful formulation of domain theories.