Теория вычислительных процессов Лекция ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ С ПОМОЩЬЮ ИНДУКТИВНЫХ УТВЕРЖДЕНИЙ Преподаватель: Веретельникова Евгения. - презентация

1 Теория вычислительных процессов Лекция ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ С ПОМОЩЬЮ ИНДУКТИВНЫХ УТВЕРЖДЕНИЙ Преподаватель: Веретельникова Евгения Леонидовна 1

2 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ ВВЕДЕНИЕ Мы сформулировали и показали на примерах, как используется метод индуктивных утверждений. И формулировки индуктивных утверждений, и процесс доказательства проводились довольно неформальным образом. Если использовать какую-либо формальную нотацию для записи индуктивных утверждений и соответствующую дедуктивную систему для проведения доказательств, то можно формализовать весь этот процесс. Обсудим некоторые аспекты такой формализации. Если мы надеемся, что в конце концов придем к тому, что при поддержке некоторой «механической» системы будем либо выполнять доказательство, либо его проверять, то некоторого типа форма- лизация нам необходима. Те, кого интересует вопрос формали- зации, могут обратиться к литературе [3, 4, 5]. Наиболее изученной формальной нотацией для формулирования и проведения математического доказательства является исчисление предикатов. 2

3 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Напомним, что метод индуктивных утверждений состоит в следующем : Для доказательства частичной правильности некоторой блок-схемы относительно утверждений А и С мы связываем утверждение А с начальной точкой блок-схемы, а утверждение С – с конечной. Кроме этого, необходимо выделить и связать с блок-схемой некоторые другие утверждения (описывающие отношения между значениями переменных, справедливые в момент попадания в соответствующую точку программы). Нужно, в частности, связать по крайней мере с одной из точек в замкнутом пути (цикле) одно такое утверждение. Затем необходимо для каждого пути в блок-схеме, ведущего из точки i с утверждением А i в точку j с утверждение А j при условии, что на пути из i в j нет промежуточных точек с утверждениями, доказать, что если мы находимся в точке i и справедливо утверждение А i а затем переходим по нашему пути в точку j, то при попадании в эту точку будет справедливо утверждение А j. 3

4 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Для формализации такого доказательства необходимо: 1) использовать некоторую формальную нотацию для записи утверждений; 2) формализовать то, что необходимо доказывать для каждого пути в блок-схеме; 3) использовать для выполнения доказательства некоторую формальную систему вывода (дедуктивную систему). Развитие формальных методов вывода для выполнения доказательств не входит в круг вопросов, рассматриваемых нами. Заинтересованный студент может познакомиться с этими вопросами в любом хорошем учебнике логики и учебном пособии [3]. Мы рассмотрим лишь вопросы, относящиеся к п. 1 и 2. Для цели, указанной в п. 1, можно использовать нотацию исчисления предикатов (или другую формальную нотацию). С ее помощью можно формулировать нужные утверждения. 4

5 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Исчисление предикатов не совсем подходит для формулирования индуктивных утверждений. Многие из них трудно (если вообще возможно) выразить с помощью этой нотации. Поиски наиболее подходящей формальной системы для записи индуктивных утверждений и проведения доказательств являются предметом современных исследований. Тем не менее здесь для выражения утверждений будет использоваться исчисление предикатов. Что касается п. 3, то надо дать некоторый систематический метод формирования для каждого из путей блок-схемы подлежащего доказательству формализованного высказывания. Множество всех таких высказываний, которые нужно доказы- вать для определения частичной правильности программы, иногда называют множеством условий верификации (verification conditions) для этой программы. 5

6 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Для систематического формирования условий верификации некоторой блок-схемы поступим следующим образом. Рассмотрим по порядку все пути в блок-схеме. Предположим, что речь идет о пути из точки i в точку j. Утверждение, относящееся к точке i, обозначим через А i (Х, Y,...), где X, Y,... – переменные, входящие в это утверждение. Аналогично обозначим и утверждение для точки j: А j (Х, Y,...). По пути из точки i в точку j значения переменных могут измениться (например, оператором присваивания). 6

7 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Для переменной V через e path (V) (изменение переменной вдоль пути) будем обозначать выражение, определяющее значение переменной V в точке j «в терминах» значений переменных в точке i и значений, присваиваемых переменным по мере прохождения пути. Если, например, на пути из i в j выполняется лишь пересылка X Y + 1, то e path (Х) = Y + 1, а e path (Y) = Y. Если на этом пути было три оператора присваивания Х X + 1, Y Y + Y и X Х + Y – 2, то e path (Х) = (Х + 1) + (Y + Y) – 2 = X + 2Y – 1 и e path (Y) = Y + Y = 2Y. Однако на пути из точки i в точку j может встретиться несколько точек, где выполняются проверки. Будем обозначать такие проверки через t k (Х, Y,...), где k – указывает точку, к которой относится проверка, а X, Y,... – переменные, от которых она зависит. 7

8 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Предположим, что t k (Х, Y,...),..., t 1 (Х, Y,...) – полный набор всех проверок, встречающихся в различных точках на пути из точки i в точку j. Для каждой из этих проверок (t m (Х, Y,...)) сформулируем высказывание :, если путь из i в j проходит по ветви, отмеченной T (истина), и, если путь из i в j проходит по ветви, отмеченной буквой F (ложь). Через path обозначается часть пути из i в j от точки i до точки m. Теперь образуем полное высказывание. Запишем формализованное условие верификации для пути из точки i в точку j: [А i (Х, Y,...) С path ] А j [e path (Х), e path (Y),...). Если на пути не встречаются проверки, то С path высказывание не включается. 8

9 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Пример Рассмотрим блок- схему, с которой мы уже имели дело раньше. Для записи утверждений, отно- сящихся к разным точкам блок-схемы, использована нотация исчисления предикатов. 9

10 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Сформируем множество условий верификации. 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). 10

11 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ 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 t p2. Отсюда условие верификации для этого пути имеет вид ( 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]. 11

12 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ 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

13 ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ Для того, чтобы закончить формализованную версию доказательства правильности данной блок-схемы методом индуктивных утверждений, остается лишь доказать справедливость каждого из этих трех верификационных условий с помощью некоторой системы вывода (дедукции). Мы не будем тратить время и обсуждать такую формальную систему. Если студент знаком с исчислением предикатов, то он может представить себе, насколько просто проводится доказательство этих условий с использованием только основных аксиом целой арифметики. 13

14 Теория вычислительных процессов Лекция АКСИОМАТИЧЕСКИЙ ПОДХОД К ДОКАЗАТЕЛЬСТВУ ЧАСТИЧНОЙ ПРАВИЛЬНОСТИ Преподаватель: Веретельникова Евгения Леонидовна 14

15 15 АКСИОМАТИЧЕСКИЙ ПОДХОД Доказательство правильности для программ, напи- санных на языках программирования, мы проводили так же, как и для блок-схем. Другими словами, мы сопоставляли с некоторыми ключевыми точками в программе индуктивные утверждения. В частности, с каждым из замкнутых путей (циклов) должно быть сопоставлено по крайней мере одно такое утверждение. Затем мы показывали, что при попадании в процессе вычислений в ту или иную точку оказывалось справедливым соответствующее утверждение. Такое доказательство частичной правильности можно провести и в другой форме.

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

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

18 18 АКСИОМАТИЧЕСКИЙ ПОДХОД Аксиома, или правило вери- фикации, которое можно использовать для доказа- тельства приведенного утверждения, гласит: Если можно доказать, что 1) {А 1 С} S1{А 2 } и 2) {А 1 С} S2{А 2 }, то отсюда можно заключить, что 3) {А 1 } IF С ТНЕN S1 ЕLSЕ S2 {А 2 }

19 19 АКСИОМАТИЧЕСКИЙ ПОДХОД Эквивалентность этой аксиомы методу индуктивных утверждений в форме, приведенной в первой части пособия, довольно очевидна. Действительно, доказывая правильность фрагмента программы, мы должны удостовериться в следующем: 1'. Если мы попали в точку 1 и справедливо утвержде- ние А 1 а затем проходим от точки 1 через точку 3 до точки 2, то А 2 справедливо. Но для этого же пути известно, что до выполнения 51 справедливы и утверждение А 1 и усло- вие С, и мы стремимся показать, что если попадем в точку 2 (т.е. если выполнение S1 закончится), то А 2 будет справедливо.

20 20 АКСИОМАТИЧЕСКИЙ ПОДХОД 2'. Если мы попадем в точку 1 и справедливо утвер- ждение А 1 а затем проходим от точки 1 через точку 4 до точки 2, то А 2 справедливо. Но для этого пути известно, что до выполнения S2 справедливо А 1 и ложно условие С (т.е. С справедливо). Мы стремимся показать, что если попадем в точку 2 (т.е. при условии окончания S2), то будет справедливо А 2. Таким образом, положения 1' и 2', которые нужно доказывать в методе индуктивных утверждений, фактически идентичны двум предусловиям 1 и 2, которые нужно доказывать, если мы хотим использовать соответствующее правило верификации.

21 21 АКСИОМАТИЧЕСКИЙ ПОДХОД Пример 2. Предположим, что мы используем язык, в котором есть оператор вида DO WHILE (C) S END; Смысл этого оператора полностью характеризуется приведенным на рисунке фрагментом блок-схемы.

22 22 АКСИОМАТИЧЕСКИЙ ПОДХОД Если нужно доказать {А 1 } Р {А 2 } где Р – такой же цикл, как DО WHILE, то можно воспользоваться следующей аксиомой или правилом верификации: Если можно доказать, что 1) {А 1 С} S{А 1 } и 2) из {А 1 С} следует А 2, то отсюда можно заключить, что 3) {А 1 } P {А 2 }.

23 23 АКСИОМАТИЧЕСКИЙ ПОДХОД Эквивалентность этой аксиомы методу индуктивных утверждений очевидна, так как при доказательстве частичной правильности нашего фрагмента блок-схемы мы должны удостовериться, что: 1'. Если мы попали в точку 1 и справедливо утверждение А 1 а затем проходим из точки 1 через точку 2 в точку 7, то снова справедливо утверждение А 1. Но для этого пути нам известно, что до выполнения S справедливы и утверждение А 1 и условие С. Мы стремимся показать, что если мы вновь попадем в точку 1 (т.е. выполнение S закончится), то А 1 будет справедливым.

24 24 АКСИОМАТИЧЕСКИЙ ПОДХОД 2.' Если мы попадем в точку 1 и справедливо условие А 1, а затем проходим из точки 1 в точку 3, то А 2 будет справедливо. Но для этого пути справедливо А 1 и ложно условие С (т. е. С справедливо). Мы стремимся показать, что из А 1 и С следует А 2. Следовательно, оба положения 1' и 2', которые нужно дока- зывать в методе индуктивных утверждений, фактически идентичны двум предусловиям 1 и 2, которые мы должны доказывать, если хотим использовать правило верификации. Приведенное правило верификации иногда записывают в менее общей форме: Если можно доказать, что 1) {А 1 С} S{А 1 }, то отсюда можно заключить, что 2) из {А 1 } P {А 1 С}, где Р – цикл вида DO WHILE.

25 25 АКСИОМАТИЧЕСКИЙ ПОДХОД Можно легко убедиться в справедливости такого варианта правила, а кроме того, и в том, что он, как и первый вариант, используется лишь для доказательства частичной правильности. Оба варианта не гарантируют, что Р когда- нибудь закончится.

26 26 АКСИОМАТИЧЕСКИЙ ПОДХОД Пример 3. Рассмотрим пример доказательства частичной правильности с помощью правил верификации. Для этого нам потребуется еще одно дополнительное правило. Предположим, что Р1, Р2 – два фрагмента программы и необходимо доказать некоторый факт, касающийся фрагмента, состоящего из Р1, за которым непосредственно следует Р2. В этом случае может оказаться полезным следующее правило верификации: Если можно доказать, что 1){А 1 } Р1 {А 2 } и 2){А 2 } Р2 {А 3 }, то отсюда можно заключить, что 3){А 1 } Р1; Р2 {А 3 }.

27 27 АКСИОМАТИЧЕСКИЙ ПОДХОД В доказательстве мы будем использовать следующую запись: {А 1 } Р {А 2 }. Это то же самое, что и запись { А 1 }Р {А 2 }. Докажем с помощью правил верификации частичную пра- вильность программы на ПЛ/1, соответствующей блок-схеме, для которой мы уже доказали частичную правильность ранее. Можно сравнить эти два доказательства и убедиться в их идентичности.

28 28 АКСИОМАТИЧЕСКИЙ ПОДХОД Фрагмент программы имеет вид /* {0 J1 1 J2} */ IQ=0; IR=J1; /* {J1= IQ J2 + IR 0 IR} */ DО WHILE (IR J1); IQ = IQ + 1; IR = IR – J2; END ; /* {J1= IQ J2 + IR 0 IR < J2} */ Мы хотим доказать, что {0 J1 1 J2} P {J1= IQ J2 + IR 0 IR < J2}, где Р – приведенный выше фрагмент программы.

29 29 АКСИОМАТИЧЕСКИЙ ПОДХОД Мы хотим доказать, что {0 J1 1 J2} P {J1= IQ J2 + IR 0 IR < J2}, где Р – приведенный выше фрагмент программы. Для этого нам нужно доказать: 1. {0 J1 1 J2} {А 1 } IQ=0; IR=J1; {J1= IQ J2 + IR 0 IR} {А 2 } Это очевидно, так как после выполнения двух операторов из этого фрагмента программы мы будем иметь IQ=0 и IR=J1, а поэтому справедливо J1= 0 J2 + J1 = J1. Кроме того, так как перед выполнением этих действий справедливо 0 J1 и значение J1 при этом не изменяется, то после их выполнения будет справедливо 0 J1 = IR.

30 30 АКСИОМАТИЧЕСКИЙ ПОДХОД 2. {J1= IQ J2 + IR 0 IR} {А 2 } DО WHILE (IR J1); IQ = IQ + 1; IR = IR – J2; END ; {J1= IQ J2 + IR 0 IR < J2} {А 3 } Для доказательства этого положения воспользуемся правилом верификации, приведенным в примере 3.2. Из правила следует, что мы сможем сделать требуемое заключение, если докажем: а) {А 2 IR J2} IQ = IQ + 1 IR = IR – J2 {А 2 }

31 31 АКСИОМАТИЧЕСКИЙ ПОДХОД Пусть переменные перед выполнением этого фрагмента программы имели значения J1 n, J2 n, IQ n и IR n. Таким образом, J1 n =IQ n J2 n + IR n и 0 IR n IR n J2 n. После выполнения программы переменные примут следующие значения: J1 n+1 = J1 n, J2 n+1 = J2 n, IQ n+1 = IQ n + 1, IR n+1 = IR n – J2 n,. Нужно показать, что J1 n+1 = = IQ n+1 J2 n+1 + IR n+1 и 0 IR n+1. Это легко сделать, подставив в наше высказывание J1 n+1, J2 n+1, IQ n+1 и IR n+1. После подстановки получим J1 n = (IQ n + 1) J2 n + (IR n – J2 n ) = IQ n J2 n + J2 n + IR n – J2 n = = IQ n J2 n + IR n и 0 IR n – J2 n или J2 n IR n. Оба утверждения по нашему предположению должны быть справедливы.

32 32 АКСИОМАТИЧЕСКИЙ ПОДХОД б) Из А 2 и (IR J1) следует А 3, т.е. из J1= IQ J2 + IR 0 IR и (IR J1) следует из J1= IQ J2 + IR 0 IR J1. Это очевидно, так как из J1= IQ J2 + IR следует J1= IQ J2 + IR, а из 0 IR и (IR J1) следует 0 IR J1. Таким образом, мы доказали: 1) {А 1 } IQ = IQ + 1 IR = IR – J2 {А 2 } 2){А 2 } DО WHILE (IR J1); IQ = IQ + 1; IR = IR – J2; END; {А 3 } и, следовательно, по правилу верификации можно заключить, что требуемое утверждение справедливо:

33 33 АКСИОМАТИЧЕСКИЙ ПОДХОД 3) {А 1 } {0 J1 1 J2} IQ = IQ + 1 IR = IR – J2 DО WHILE (IR J1); IQ = IQ + 1; IR = IR – J2; END; {А 3 } { J1= IQ J2 + IR 0 IR J1} Можно легко убедиться, что доказательство с помощью правил верификации фактически идентично доказательству, которое можно было бы провести методом индуктивных утверждений.

34 34 АКСИОМАТИЧЕСКИЙ ПОДХОД В качестве упражнения представьте, что в используемом языке программирования есть оператор вида REPEAT S UNTIL С. Этот оператор имеет традиционный для языков программирования смысл: он эквивалентен приведенной на рисунке блок-схеме. Сформулируйте правило верификации для доказательства справедливости {А 1 } REPEAT S UNTIL С{А 2 }.