Синтез программ: от математических требований к автоматическому построению кода.
Program synthesis
Синтез программ: автоматическое создание кода по формальной спецификации. Методы, применение в оптимизации и проверке корректности. Автоматизация разработки.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Задача построения программы, соответствующей формальной спецификации.
В информатике, синтез программы — это задача создания программы, которая доказанно удовлетворяет заданной формальной спецификации высокого уровня. В отличие от верификации программы, программа должна быть построена, а не предоставлена; однако, обе области используют методы формального доказательства и включают подходы различной степени автоматизации. В отличие от техник автоматического программирования, спецификации в синтезе программ обычно представляют собой неалгоритмические утверждения, выраженные на соответствующем языке логического исчисления. Основное применение синтеза программ — освобождение программиста от необходимости написания корректного и эффективного кода, удовлетворяющего спецификации. Тем не менее, синтез программ также находит применение в супероптимизации и выводе инвариантов циклов.
Task to construct a program meeting a formal specification
In computer science, program synthesis is the task to construct a program that provably satisfies a given high level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automation. In contrast to automatic programming techniques, specifications in program synthesis are usually non algorithmic statements in an appropriate logical calculus. The primary application of program synthesis is to relieve the programmer of the burden of writing correct, efficient code that satisfies a specification. However, program synthesis also has applications to superoptimization and inference of loop invariants.
Происхождение
Во время Летнего института символической логики в Корнелльском университете в 1957 году Алонзо Черч сформулировал задачу синтеза схемы на основе математических требований. Несмотря на то, что в работе рассматриваются только схемы, а не программы, она считается одним из первых описаний синтеза программ, и некоторые исследователи называют синтез программ «проблемой Черча». В 1960-х годах аналогичная идея «автоматического программиста» изучалась исследователями в области искусственного интеллекта. С тех пор различные научные сообщества занимались проблемой синтеза программ. Примечательными работами являются теоретический подход к автоматам 1969 года, предложенный Бюхи и Ландвебером, а также работы Манны и Вальдингера (около 1980 года). Развитие современных языков программирования высокого уровня также можно рассматривать как форму синтеза программ.
During the Summer Institute of Symbolic Logic at Cornell University in 1957, Alonzo Church defined the problem to synthesize a circuit from mathematical requirements. Even though the work only refers to circuits and not programs, the work is considered to be one of the earliest descriptions of program synthesis and some researchers refer to program synthesis as "Church's Problem". In the 1960s, a similar idea for an "automatic programmer" was explored by researchers in artificial intelligence. Since then, various research communities considered the problem of program synthesis. Notable works include the 1969 automata theoretic approach by Büchi and Landweber, and the works by Manna and Waldinger (c. 1980). The development of modern high level programming languages can also be understood as a form of program synthesis.
Развитие XXI века
В начале XXI века наблюдается резкий рост практического интереса к идее синтеза программ в сообществе формальной верификации и смежных областях. Армандо Солар Лезама показал, что задачи синтеза программ можно кодировать в булевой логике и использовать алгоритмы решения задачи выполнимости булевых формул для автоматического поиска программ.
The early 21st century has seen a surge of practical interest in the idea of program synthesis in the formal verification community and related fields. Armando Solar Lezama showed that it is possible to encode program synthesis problems in Boolean logic and use algorithms for the Boolean satisfiability problem to automatically find programs.