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

,

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

,

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

[Аi (Х, Y, ...) Λ С 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 Λ 1 ≤ J2) → [ер1 (J1) = ер1 (IQ) ● ер1 (J2) + ер1 (IR) Λ 0 ≤ ер1 (IR)],

( 0 ≤ J1  Λ  1 ≤ J2 ) → ( J1 = IQ ● J2 + J1 Λ  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  Λ  0 ≤ IR  Λ J2 ≤ IR ) →
→ [ер2 (J1) = ер2 (IQ) ● ер2 (J2) + ер2 (IR)  Λ  0 ≤ ер2 (IR)],

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

(J1 = IQ ● J2 + IR Λ 0 ≤ IR Λ J2 ≤ IR) →
→ [J1 = (IQ + 1) ● J2 + (IR – J2) Λ 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 Λ 0≤IR Λ IR<J2) → (J1 = IQ●J2+IR Λ 0<IR Λ 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 Λ С} S1{А2}

и

2)  {А1 Λ ¬ С} 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.

Таким образом, положения 1' и 2', которые нужно доказывать в методе индуктивных утверждений, фактически идентичны двум предусловиям 1 и 2, которые нужно доказывать, если мы хотим использовать соответствующее правило верификации.

Рис. 3.2

Пример 3.2. Предположим, что мы используем язык, в котором есть оператор вида

DO  WHILE  (C)

  S

END;

Смысл этого оператора полностью характеризуется приведенным на рис. 3.2 фрагментом блок-схемы. Если нужно доказать {А1} Р {А2} где Р – такой же цикл, как DО WHILE, то можно воспользоваться следующей аксиомой или правилом верификации: Если можно доказать, что

1)  {А1 Λ С} S{А1}

и

2) из {А1 Λ ¬ С} следует  А2,

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

3) {А1} P {А2}.

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

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

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

Следовательно, оба положения 1' и 2', которые нужно доказывать в методе индуктивных утверждений, фактически идентичны двум предусловиям 1 и 2, которые мы должны доказывать, если хотим использовать правило верификации.

Приведенное правило верификации иногда записывают в менее общей форме:

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

1)  {А1 Λ С} S{А1},

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

2) из {А1} P {А1 Λ ¬ С}, где Р – цикл вида DO  WHILE.

Студент может легко убедиться в справедливости такого варианта правила, а кроме того, и в том, что он, как и первый вариант, используется лишь для доказательства частичной правильности. Оба варианта не гарантируют, что Р когда-нибудь закончится.

Пример 3.3. Рассмотрим пример доказательства частичной правильности с помощью правил верификации. Для этого нам потребуется еще одно дополнительное правило. Предположим, что Р1, Р2 – два фрагмента программы и необходимо доказать некоторый факт, касающийся фрагмента, состоящего из Р1, за которым непосредственно следует Р2. В этом случае может оказаться полезным следующее правило верификации:

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

1)        {А1}  Р1  {А2}

и

2)        {А2} Р2 {А3} ,

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

3)        {А1} Р1; Р2 {А3} .

В доказательстве мы будем использовать следующую запись:

{А1}

Р

{А2}.

Это то же самое, что и запись  { А1}Р {А2}.

Докажем с помощью правил верификации частичную правильность программы на ПЛ/1, соответствующей блок-схеме, для которой мы уже доказали частичную правильность в примере 2.3 в первой части учебного пособия [2]. Студент может сравнить эти два дока­зательства и убедиться в их идентичности. Фрагмент программы имеет вид