English
!

Архив публикаций

Тезисы

XVIII-ая конференция

Методы автоматизированного построения программ

Корухова Ю.С.

МГУ им. М.В. Ломоносова, факультет ВМК, 2 учебный корпус, Ленинские горы, Москва, ГСП-1, 119991, Российская Федерация

2  стр. (принято к публикации)

В настоящее время компьютеры используются в самых разных областях, но в любой из них для компьютера решение задачи ― это выполнение некоторой программы, реализующей алгоритм решения. На практике процесс решения любой задачи начинается не с разработки алгоритма, а с анализа требований, то есть условий, ограничений, описывающих, как связаны исходные данные и результат. Запись этих требований называется спецификацией. В докладе будет рассмотрено автоматизированное построение (синтез) программ по их спецификациям. Мы используем два подхода к синтезу ― дедуктивный и построение программ на основе предыдущего опыта (рассуждения на основе прецедентов).

При дедуктивном подходе спецификация представляет собой математическую теорему, которую требуется конструктивно доказать. Методы дедуктивного синтеза каждому шагу доказательства ставят в соответствие построение некоторой конструкции программы. Полученная с помощью данного подхода программа не требует дальнейшей верификации, так как одновременно с синтезом доказывается её соответствие всем заданным в спецификации требованиям. Однако известные методы синтеза обладают общим недостатком: при их автоматизированном применении возникает огромный перебор вариантов доказательств. Возможными вариантами сокращения такого перебора являются планирование доказательства, комбинирование различных схем синтеза, применение эвристик, выделение фрагментов, которые можно синтезировать параллельно.

Другим подходом является использование рассуждений на основе прецедентов. Прецедент представляет собой пару: спецификация ― текст программы, на некотором языке программирования. Для решения новой задачи вводится ее спецификация, и для нее выбирается наиболее похожая задача из библиотеки прецедентов. Затем происходит адаптация имеющегося решения. Проверка полученного решения осуществляется либо пользователем, либо же автоматизированной системой.

Комбинирование различных подходов к синтезу позволяет расширить класс программ, которые могут быть построены автоматизированно.


Литература.

1. Korukhova Y. An approach to automatic deductive synthesis of functional programs.// Annals of Mathematics and Artificial Intelligence, Vol. 50: 3-4 – Springer, 2007, p.255-271

2. Korukhova Y., Fastovets N. A Case-Based Reasoning Approach to Program Synthesis// Proceedings of The International Conference Knowledge Engineering and Ontology Development (KEOD), 2010.



© 2004 Дизайн Лицея Информационных технологий №1533