История развития синтеза программ

Начало автоматическому синтезу программ было положено в 1960;е гг., и первоначально синтез программ не отделялся от обычной трансляции языков программирования.

С появлением метода резолюций дедуктивный синтез программ резко выделился из общего потока работ по автоматизации программирования за счет использования аппарата математической логики.

В 1970;е гг. наблюдался повышенный интерес к этой тематике, были получены значительные результаты. Появились аксиоматика Хоара и денотационная семантика Скотта.

Смысл аксиомы оператора присваивания заключается в том, что после выполнения присваивания постусловие {Р} имеет то же истинностное значение, что и предусловие {Р[Е/х]}. Например,.

Правило композиции применяется к последовательному выполнению программ S и Т, что записывается как S] Т:

Например,

Правило условного оператора:

Например, абсолютная величина числа:

Правило оператора цикла:

Здесь Р является инвариантом цикла.

Например, деление вычитанием:

что на ноль делить нельзя. Доказательство завершаемое™ приходится проводить отдельно, что не всегда просто, а иногда и невозможно.

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

Сэр Чарльз Энтони Ричард Хоар (Charles Antony Richard Hoare), родился в 1934 г. — британский ученый, специализирующийся в области информатики и вычислительной техники. Наиболее известен как разработчик алгоритма «быстрой сортировки».

В 2000 г. он был удостоен рыцарского титула за заслуги в области образования и компьютерных наук.

«Но существует одно качество, которое нельзя купить, — это надежность. Цена надежности — погоня за крайней простотой. Это цепа, которую очень богатому труднее всего заплатить».

Дана Стюарт Скотт (Dana Stewart Scott), родился в 1932 г. — американский ученый в области математики и информатики.

Исследования Скотта связаны с теорией моделей, теорией автоматов, модальной и интуиционистской логиками, конструктивной математикой и связью между логикой и теорией категорий. Философские интересы лежат в области оснований логики, философии математики и семантического анализа естественных языков. Работы в области информатики направлены на разработку денотационной семантики языков программирования и математических основ вычислимости.

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

Затем, в 1980;е гг., наблюдался некоторый спад интереса к этой тематике, и в то же время работы велись, и были получены исчерпывающие ответы на некоторые вопросы синтеза программ. В частности, Н. Н. Непейвода и другие исследователи показали, что из интуиционистского доказательства теоремы существования определенного вида автоматически и эффективно извлекается программа на обычном императивном языке программирования^[1]. Тем самым задача автоматического синтеза программ была сведена к задаче автоматического доказательства теорем.

Николай Николаевич Непейвода, родился в 1949 г. — математик, логик, философ, информатик.

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

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

В 1990;е гг. наблюдался застой. По мнению автора, это связано с тем, что доминирование объектно-ориентированного программирования не способствовало автоматическому синтезу программ.

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

Дедуктивный синтез программ — наиболее развитый в настоящее время вид автоматического синтеза программ, поэтому общие сведения о синтезе программ мы приводим с использованием примеров из дедуктивного синтеза.

• [1] Непейвода II. II. О построении правильных программ // Вопросы кибернетики. 1978.№ 46. С. 88−122.