Cтраница 4
Класс встроенных MV-зависимостей был обнаружен в работах Fagin [ 1977с ] и Delobel [1978], а в работах Parker, Parsaye-Ghomi [1980], Sadiv, Waiecka [1979] было показано, что для класса одних EMV-зависимостей не существует полной, конечной аксиоматизации. Процедуру доказательства вы водимости для более широкого класса зависимостей, которые определены в гл. В работах Beeri, Vardi [ 1980a, b ], а также Chandra, Lewis, Makowsky [1981] показано, что выводимость для этого класса зависимостей неразрешима. Здесь нет противоречия, поскольку процедура доказательства выводимости включает как конечные, так и бесконечные отношения. Утверждение о выводимости может иметь бесконечный контрпример и не иметь конечного. [46]
В приведенных выше примерах мы показали, что заключения следуют из данных фактов. Обоснование того, как заключение следует из аксиом, называется доказательством. Процедура нахождения доказательств называется процедурой доказательства. В главах 4 - 9 мы дадим такие процедуры доказательств, которые для нахождения доказательства механически используют правила вывода. Эти процедуры доказательств очень эффективны. Читатель легко обнаружит, что три предыдущих примера чрезвычайно легко доказать, если использовать такие процедуры доказательств. [47]
Следует обратить внимание на то, что доказательство общей правильности программы проводится не путем анализа результатов ее прогона, а на основе анализа программы, как статического математического объекта, на который распространяются аксиомы и правила логического вывода. Основной проблемой доказательства правильности программы является формирование вспомогательных утверждений. Для этого требуется тщательный учет структуры программы и семантики языка программирования. Построения вспомогательных утверждений для некоторой произвольной программы зачастую оказываются очень сложной и конструктивной задачей, поэтому определенные преимущества достигаются тогда, когда процедуры доказательства и правильности программы разрабатываются в процессе ее проектирования. Чтобы доказать факт завершения работы программы, необходимо доказать, во-первых, что программа не остановлена преждевременно, и, во-вторых, что программа не зациклилась. Подтверждение первого факта может оказаться очень сложным, например, может возникнуть потребность в доказательстве того, что не будет происходить арифметического переполнения. Подтверждение того, что программа в конце концов выйдет из некоторого цикла, может быть основано на концепции вполне упорядоченного множества ( W. Допустим, например, что применительно к некоторому циклу выражение Е может быть найдено так, что если оно отрицательно, цикл немедленно завершится. Далее допустим, что может быть доказан факт уменьшения Е с каждой итерацией цикла. Из этого следует, что цикл должен завершиться. Доказательство правильности программы не дает полного решения проблемы надежности программного обеспечения практически используемых систем. [48]
В доказательстве используются три правила вывода: подстановка, замена, отделение, а в качестве аксиом - пять истинных высказываний. Построение доказательства начинается от конечного результата по направлению к исходным посылкам. Эта направленность доказательства и вопросы иерархического цепеобра-зования в доказательстве теорем имеют ряд общих черт с процедурой синтеза структуры ХТС. На каждом этапе из заданного списка аксиом или ранее доказанных теорем выбирается такая теорема, из которой с помощью правил вывода может быть выведена теорема данного этапа. Поэтапная процедура доказательства продолжается до тех пор, пока в списке для вывода не окажутся исходные посылки. В этом случае проблема считается решенной. Необходимо однако отметить, что в ряде случаев поиск метода доказательства теорем может оказаться также и безуспешным. [49]
В приведенных выше примерах мы показали, что заключения следуют из данных фактов. Обоснование того, как заключение следует из аксиом, называется доказательством. Процедура нахождения доказательств называется процедурой доказательства. В главах 4 - 9 мы дадим такие процедуры доказательств, которые для нахождения доказательства механически используют правила вывода. Эти процедуры доказательств очень эффективны. Читатель легко обнаружит, что три предыдущих примера чрезвычайно легко доказать, если использовать такие процедуры доказательств. [50]