Кіріспе
Формалды талаптарға сай бағдарлама құру міндеті. Компьютер ғылымында бағдарламалық синтез – берілген жоғары деңгейдегі формалды талаптарды нақты орындайтын бағдарламаны құру міндеті. Бағдарламаны тексеруден өзгешелігі, бағдарлама берілмей, құрастырылады; алайда, екі сала да формалды дәлелдеу әдістерін пайдаланады және әртүрлі деңгейде автоматтандырылған тәсілдерді қамтиды. Автоматты бағдарламалау техникаларынан айырмашылығы, бағдарламалық синтездегі талаптар көбінесе тиісті логикалық есептеулерде алгоритмдік емес тұжырымдар болып табылады. Бағдарламалық синтездің басты мақсаты – бағдарламашыны талаптарға сәйкес дұрыс, тиімді код жазу қиындығынан босату. Дегенмен, бағдарламалық синтез супероптимизация және цикл инварианттарын шығару салаларында да қолданылады.
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 ж.) бар. Қазіргі заманғы жоғары деңгейдегі бағдарламалау тілдерінің дамуын бағдарламалық синтездің бір түрі деп қарастыруға болады.
ХХІ ғасырдағы өзгерістер
ХХІ ғасырдың басында ресми тексеру қауымдастығы және оған байланысты салаларда бағдарлама синтезі идеясына қызығушылық күрт артты. Армандо Солар Лезама бағдарлама синтезі мәселелерін Буль логикасында бейнелеуге және Буль қанағаттандыру мәселесін шешетін алгоритмдерді пайдаланып бағдарламаларды автоматты түрде табуға болатынын көрсетті.