프로그램 합성

프로그램 합성(Program synthesis)은 컴퓨터 과학에서 주어진 높은 수준의 형식 사양을 확실히 만족시키는 프로그램을 구성하는 작업이다. 프로그램 검증과 달리 프로그램은 제공되기보다는 구성된다. 그러나 두 분야 모두 형식 증명 기술을 사용하며 둘 다 서로 다른 수준의 자동화 접근 방식으로 구성된다. 자동 프로그래밍 기술과 달리 프로그램 합성의 사양은 일반적으로 적절한 논리 계산의 비알고리즘 진술이다.

프로그램 합성의 주요 응용 프로그램은 사양을 충족하는 정확하고 효율적인 코드를 작성해야 하는 프로그래머의 부담을 덜어주는 것이다. 그러나 프로그램 합성에는 루프 불변량의 초최적화 및 추론에도 적용할 수 있다.

같이 보기

• 귀납적 프로그래밍
• 메타프로그래밍

출처

• Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando (2018년 11월 20일). “Search-based program synthesis”. 《Communications of the ACM》 61 (12): 84–93. doi:10.1145/3208071. ISSN 0001-0782. 
• Zohar Manna, Richard Waldinger (1975). “Knowledge and Reasoning in Program Synthesis”. 《Artificial Intelligence》 6 (2): 175–208. doi:10.1016/0004-3702(75)90008-9.