Минашин Георгий Алексеевич

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

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