ПРОГРА́ММ СИ́НТЕЗ
-
Рубрика: Математика
-
Скопировать библиографическую ссылку:
ПРОГРА́ММ СИ́НТЕЗ, процесс так называемого доказательного программирования, когда составление программы сопровождается доказательством её соответствия формальной постановке исходной задачи. На практике П. с. объединяет в себе три типа формальных манипуляций с программами: логич. синтез, сборку и конкретизацию.
Логический синтез – один из способов перехода от программы спецификации к реализующему алгоритму, имеющий форму точного рассуждения в некоторой логич. системе. Одной из логич. систем является конструктивная логика, где синтезируемая программа извлекается из конструктивного доказательства теоремы о существовании решения задачи. Другой тип логич. системы – логики Хоара (см. в ст. Программ верификация).
Сборка – особый случай логич. синтеза, когда элементами конструирования программы являются сравнительно крупные программные заготовки – т. н. модули программ. Спецификация частной задачи при сборке задаётся в виде указания аргументов и результатов на т. н. вычислит. модели, характеризующей класс синтезируемых программ и задающей правила сочетаемости модулей при сборке программ. Возникающая при этом логич. система обладает свойством разрешимости, что позволяет в ряде случаев осуществлять сборку программы автоматически.
При конкретизации результирующая программа получается путём сужения универсального алгоритма на особые условия его применения, характеризующие частную задачу, подлежащую решению.
Существенную роль во всех видах П. с. играет программ оптимизация, основанная на формальных эквивалентных преобразованиях текстов программ.