ВКР: Синтез программ по спецификациям с множественными вызовами

Оглавление

• Синтез по спецификациям с множественными вызовами 28 4.1. Доказательство нереализуемости спецификации . . . . . 28

4.2. Поиск ветвей синтезируемой функции с множественными вызовами............................ 30

4.3. Абдукция............................ 31

4.4. Алгоритм синтеза, использующий одну ветку . . . . . . . 32

4.5. Алгоритм синтеза, использующий несколько веток одно-

временно ............................ 35




3














































4

Введение

Широко известна задача автоматического создания программ на некотором языке программирования, которые удовлетворяют намере-ниям пользователя, выраженным в форме ограничений [7, 10, 21]. Она называется задачей синтеза программ. Качественный синтез программ делает процесс разработки более надежным и менее трудоёмким. Она лежит на стыке следующих областей — искусственного интеллекта, ма-шинного обучения, формальной верификации, математической логики.

Среди известных подходов к синтезу программ существует эффек-тивный и хорошо масштабируемый подход, называемый функциональ-ным синтезом [8, 9, 15, 16, 17, 18, 19, 27, 30, 35]. В рамках этого подхода синтезируемая программа рассматривается как функция, а намерения пользователя выражаются в виде утверждений на языке исчисления предикатов первого порядка, называемых спецификацией программы, которая связывает входные и выходные параметры функции.

Функциональный синтез накладывает сильные ограничения на фор-мат спецификации. Существующие методы функционального синтеза основываются на эффективных алгоритмах устранения кванторов [8, 15, 16, 17, 19, 27, 30, 35]. Однако в настоящий момент они хорошо ра-ботают только для спецификаций, в которых синтезируемая функция встречается только с одним и тем же фиксированным набором аргу-ментов