Лекция 10

КОНЦЕПЦИЯ ДОКАЗАТЕЛЬНОГО ПРОГРАММИРОВАНИЯ

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

Подход к автоматизации программирования, получивший название автоматический синтез программ, выделился, начиная с 70-х годов в самостоятельную область исследований. Основная цель исследований и разработок в этой области состоит в том, чтобы использовать ЭВМ в процессе программирования путем передачи машине (автоматизации) отдельных видов работ, входящих в цикл создания программы - от возникновения замысла алгоритма до анализа и получения результата.

Логико-математические подходы к реализации перехода от спецификации задачи к программам (для различных моделей вычислений), гарантирующих корректность такого перехода в том смысле, как понимается правильность доказательства в математике, объединены под общим названием - доказательное программирование [13], [16], [18], [57], [58], [69], [89], [150].

Следует отметить, что необходимость создания более убедительного (по сравнению с традиционной отладкой) способа гарантии правильности программм была осознана еще в 60-е годы, когда появились первые работы, приведшие к созданию верификационного подхода. Основная идея верификации программ [71] заключается в том, чтобы вместо отладки и тестирования определять математическое доказательство правильности соответствия текста программы ее исходной спецификации. Первые работы в этом направлении [125], [133] предлагали связывать с началом и концом работы программы P логические утверждения i и j и доказывать, что если для входных данных выполняется условие i и P на этих данных заканчивает работу, то выходные данные будут удовлетворять условию j. В данном случае говорили о частичной корректности P по отношению к i и j - в формальной записи i{P}j. Если же удавалось доказать, что P не только частично корректно, но и заканчивает свою работу при всех данных, удовлетворяющи i, то P называлась тотально корректной по отношению к i и j (i[P]j). Основной трудностью при верификации является выявление закономерностей, относящихся к значению переменных, входящих в циклические и рекурсивные структуры функции (инварианты циклов и рекурсий). Есле же такие закономерности выявлены, то тот факт, что они сохраняются при выполнении соответствующих им операторов можно уже доказывать методом, аналогичным методу математической индукции. В этом и состояла первоначальная идея Флойда и Наура. Сами формулировки индуктивных утверждений и процесс доказательтства в их работах осуществлялись неформальным образом. Чтобы строить "механические" системы верификации программ, необходимы были формальные дедуктивные системы в языке, и средствами которых можно было бы записывать индуктивные утверждения, так и строя доказательство. Первую такую систему указал Хоар [133]. Дальнейшие исследования в области верификационного программирования осуществлялись в следующих трех направлениях (см. обзоры [4], [70]):

а) поиск новых методов доказательства частичной и полной корректности программ;

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

в) автоматизация процесса верификации программ, создание практических верификационных систем.

Работы по верификационному программированию послужили толчком для исследований в области аксиоматической семантики языков программирования, которые, в свою очередь, привели к созданию Дейкстрой нового метода доказательного программирования, который мы назовем методом Дейкстры [1], [13], [16].

В данном подходе каждый оператор S в фоннеймановских программах интерпретируется не только как преобразователь данных, но и как преобразователь условий (предикатов), причем, образно говоря, преобразование предикатов обратно по своему направлению преобразованию данных. Это наблюдение позволило поставить задачу поиска для оператора S и выходного условия j такого предусловия wp(S,j), чтобы выполнилось утверждение wp(S,j){S}j, и, если ф{S}j, то была бы истинна импликация (i wp(S,j)), (в силу этих условий предикат wp(S,j) называется слабейшим предусловием для S и j). Понятие слабейшего предусловия позволило Дейкстре создать метод программирования, где правильность программы доказывается одновременно с ее конструированием. Основу этого метода составляет процедура последовательного преобразования целевого предиката j в последовательность слабейших предусловий вместе с соответствующими этим предусловиям программными конструкциями и доказательством того, что эти предусловия логически следуют из заданного спецификационного предусловия i на входные данные.

К дедуктивным подходам решения задач относится и концептуальное программирование. Этот метод ориентирован в основном на решение так называемых вычислительных задач: при заданном описании условий задачи M по значениям переменных

x__1__,x__2__,...,x__m__, удовлетворяющих M, вычислить значения переменных

y__1__,y__2__,...,y__n__, также удовлетворяющих M.

Основу концептуального программирования составляет метод структурного синтеза программ, использующий две эквивалентные формы представления знаний о задачах - формульное и графовое представление [12].

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

В методе структурного синтеза программ используются аксиомы следующих видов:

1) простейшее предложение вычислимости

a -> b,

f

где a, b -конечные множества переменных, f - функция вычислимости, по которой, зная переменные a, можно вычислить b;

2) предложение вычислимости с условием

P => a -> b,

f

где P - формула, выражающая условия, при которых возможно вычисление b из a;

3) предложения вычислимости с подзадачей

h( u -> y => a -> b ),

h f(h)

где - квантор существования, h - функциональная переменная подзадачи.

Сформулировав условия задачи в виде предложений вычислимости, строят доказательство теоремы

f(u -> v),

f

где u - исходные, а v - искомые данные задачи. Для доказательства в качестве правил вывода используются правила структурного синтеза [176]. При извлечении программы из доказательства каждому правилу вывода ставится в соответствие некоторый оператор программы.

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

Из практических систем концептуального программирования следует прежде всего отметить систему ПРИЗ [40], [95], объектно-ориентированный язык НУТ [157], синтезирующий в себе идеи таких языков, как УТОПИСТ, Пролог и Смолток, а также СПОРА [5], МАВР [86].