Доказательство правильности программ (стр. 3 )

1) использовать некоторую формальную нотацию для записи утверждений;

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

3) использовать для выполнения доказательства некоторую формальную систему вывода (дедуктивную систему).

Развитие формальных методов вывода для выполнения доказательств не входит в круг вопросов, рассматриваемых в данном учебном пособии. Заинтересованный студент может познакомиться с этими вопросами в любом хорошем учебнике логики и учебном пособии [3]. Мы рассмотрим лишь вопросы, относящиеся к п. 1 и 2. Для цели, указанной в п. 1, можно использовать нотацию исчисления предикатов (или другую формальную нотацию). С ее помощью можно формулировать нужные утверждения. Исчисление предикатов не совсем подходит для формулирования индуктивных утверждений. Многие из них трудно (если вообще возможно) выразить с помощью этой нотации. Поиски наиболее подходящей формальной системы для записи индуктивных утверждений и проведения доказательств являются предметом современных исследований. Тем не менее здесь для выражения утверждений будет использоваться исчисление предикатов. Что касается п. 3, то надо дать некоторый систематический метод формирования для каждого из путей блок-схемы подлежащего доказательству формализованного высказывания. Множество всех таких высказываний, которые нужно доказывать для определения частичной правильности программы, иногда называют множеством условий верификации (verification conditions) для этой программы.

Для систематического формирования условий верификации некоторой блок-схемы поступим следующим образом. Рассмотрим по порядку все пути в блок-схеме. Предположим, что речь идет о пути из точки i в точку j. Утверждение, относящееся к точке i, обозначим через Аi (Х, Y, ...), где X, Y, ... – переменные, входящие в это утверждение. Аналогично обозначим и утверждение для точки j: Аj (Х, Y, ...). По пути из точки i в точку j значения переменных могут измениться (например, оператором присваивания). Для переменной V через epath (V) (изменение переменной вдоль пути) будем обозначать выражение, определяющее значение переменной V в точке j «в терминах» значений переменных в точке i и значений, присваиваемых переменным по мере прохождения пути. Если, например, на пути из i в j выполняется лишь пересылка X Y + 1, то epath (Х) = Y + 1, а epath (Y) = Y. Если на этом пути было три оператора присваивания Х X + 1,
Y Y + Y и X Х + Y – 2, то epath (Х) = (Х + 1) + (Y + Y) – 2 =
= X + 2•Y – 1 и epath (Y) = Y + Y = 2•Y. Однако на пути из точки i в точку j может встретиться несколько точек, где выполняются проверки. Будем обозначать такие проверки через tk (Х, Y, ...), где k – указывает точку, к которой относится проверка, а X, Y, ... – переменные, от которых она зависит. Предположим, что tk  (Х, Y, ...), ..., t1  (Х, Y, ...) – полный набор всех проверок, встречающихся в различных точках на пути из точки i в точку j. Для каждой из этих проверок (tm  (Х, Y, ...)) сформулируем высказывание:

,

если путь из i в j проходит по ветви, отмеченной T (истина), и

,

если путь из i в j проходит по ветви, отмеченной буквой F (ложь). Через path’ обозначается часть пути из i в j от точки i до точки m. Теперь образуем полное высказывание . Запишем формализованное условие верификации для пути из точки i в точку j:

[Аi (Х, Y, ...) L С path] ® Аj [e path (Х), e path (Y), ...).

Если на пути не встречаются проверки, то С path высказывание не включается.

Пример 2.1. Рассмотрим блок-схему (рис. 2.1), с которой мы уже имели дело в примере 2.3 в первой части учебного пособия [2]. Для записи утверждений, относящихся к разным точкам блок-схемы, использована нотация исчисления предикатов.

Сформируем множество условий верификации.

1. Путь из точки 1 в точку 2 назовем р1. Для этого пути имеем ер1 (J1) = J1, ер1 (J2) = J2, ер1 (IQ) = 0, ер1 (IR) = J1. Так как по пути проверки не выполняется, то можно написать следующее условие верификации для этого пути:

(0 £ J1 L 1 £ J2) ® [ер1 (J1) = ер1 (IQ) · ер1 (J2) + ер1 (IR) L 0 £ ер1 (IR)],

( 0 £ J1 L 1 £ J2 ) ® ( J1 = IQ · J2 + J1 L 0 £ J1).

2. Путь из точки 2 через точки 3, 4 в точку 2 обозначим через р2. Для этого пути имеем ер2 (J1) = J1, ер2 (J2) = J2, ер2 (IQ) = IQ + 1, ер2 (IR) = IR – J2.

На пути есть только одна проверка IR < J2. Ту часть пути р2, которая ведет от точки 2 до этой проверки, обозначим через р2'. Так как путь р2 после проверки проходит по ветви, отмеченной F, то

.

Поскольку проверка только одна, получаем

Сp2 º Ø tp2.

Отсюда условие верификации для этого пути имеет вид

( J1 = IQ · J2 + IR L 0 £ IR L J2 £ IR ) ®
® [ер2 (J1) = ер2 (IQ) · ер2 (J2) + ер2 (IR) L 0 £ ер2 (IR)],

или после преобразования

(J1 = IQ · J2 + IR L 0 £ IR L J2 £ IR) ®
® [J1 = (IQ + 1) · J2 + (IR – J2) L 0 < IR – J2].

Рис. 2.1

3. Путь из точки 2 через 5 в точку 6 обозначим через рЗ. Для этого пути имеем ер3 (J1) = J1, ер3 (J2) = J2, ер3 (IQ) = IQ, ер3 (IR) = IR. На пути встречается лишь одна проверка IR < J2.

Часть пути от точки 2 до этой проверки обозначим через р3'. Как и выше, имеем ер3' (IR) = IR и ер3' (J2) = J2. Так как после проверки путь проходит по ветви, обозначенной Т (истина), то

.

Следовательно, условие верификации для всего пути имеет вид

(J1 = IQ·J2+IR L 0£IR L IR<J2) ® (J1 = IQ·J2+IR L 0<IR L IR<J2).

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

Глава 3. АКСИОМАТИЧЕСКИЙ ПОДХОД
К ДОКАЗАТЕЛЬСТВУ ЧАСТИЧНОЙ ПРАВИЛЬНОСТИ

Доказательство правильности для программ, написанных на языках программирования, в первой части учебного пособия мы проводили так же, как и для блок-схем. Другими словами, мы сопоставляли с некоторыми ключевыми точками в программе индуктивные утверждения. В частности, с каждым из замкнутых путей (циклов) должно быть сопоставлено по крайней мере одно такое утверждение. Затем мы показывали, что при попадании в процессе вычислений в ту или иную точку оказывалось справедливым соответствующее утверждение. Такое доказа­тельство частичной правильности можно провести и в другой форме. Можно показать, что доказательство основывается на некоторых аксиомах или правилах верификации. В этом разделе рассмотрены правила верификации и показана их экви­валентность методу индуктивных утверждений. Мы не при­водим полного множества правил верификации для какого-нибудь языка, а лишь на двух примерах поясним основную идею. Для записи правил верификации используем следующую нотацию: {А1} Р {А2}, где А1 и А2 – утверждения (индуктивные), а Р – фрагмент программы из одного или нескольких операторов. Такая запись означает, что если непосредственно перед выполнением Р справедливо А1 то после выполнения Р (если оно закончится) будет справедливо А2. Теперь перейдем к примерам правил верификации.

Пример 3.1. Представим себе, что в используемом нами языке есть оператор вида IF С ТНЕN S1 ЕLSЕ S2 и мы хотим доказать (как часть некоторого доказательства правильности), что {А1} IF С ТНЕN S1 ЕLSЕ S2 {А2}. Другими словами, нужно доказать, что если непосредственно перед выполнением этого оператора было справедливо А1 а затем закончилось выполнение оператора, то непосредственно после этого будет справедлива А2. Мы предполагаем, что оператор имеет смысл, традиционный для языков программирования, т. е. он эквивалентен приведенному на рис. 3.1 фрагменту блок-схемы. Аксиома, или правило верификации, которое можно использовать для доказательства приведенного утверждения, гласит:

Рис. 3.1.

Если можно доказать, что

1) {А1 L С} S1{А2}

и

2) {А1 L Ø С} S2{А2},

то отсюда можно заключить, что

3) {А1} IF С ТНЕN S1 ЕLSЕ S2 {А2}.

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

1'. Если мы попали в точку 1 и справедливо утверждение А1 а затем проходим от точки 1 через точку 3 до точки 2, то А2 справедливо. Но для этого же пути известно, что до выполнения 51 справедливы и утверждение А1 и условие С, и мы стремимся показать, что если попадем в точку 2 (т. е. если выполнение S1 закончится), то А2 будет справедливо.

2'. Если мы попадем в точку 1 и справедливо утверждение А1 а затем проходим от точки 1 через точку 4 до точки 2, то А2 справедливо. Но для этого пути известно, что до выполнения S2 справедливо А1 и ложно условие С (т. е. Ø С справедливо). Мы стремимся показать, что если попадем в точку 2 (т. е. при условии окончания S2), то будет справедливо А2.