Теория вычислительных процессов Лекция Метод индуктивных утверждений Преподаватель: Веретельникова Евгения Леонидовна 1

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

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

Метод индуктивных утверждений Трудность заключается в том, что это не просто проход по элемен- тарному циклу и возврат в точку 1. Перед возвратом в точку 1 несколько раз будет выполняться внутренний цикл. Следо­вательно, первым, вероятно, нужно доказать утверждение 2, а затем уже исполь- зовать его для доказательства того, что при возврате в точку 1 утверж- дение 1 останется справедливым. Пытаясь, однако, доказать справедливость утверждения 2 при каждом попадании в точку 2, мы сталкиваемся с аналогичными трудностями. Фактически нужно показать, что при любом попадании в точку 2 из точки 1 (не только в первый момент) будет справедливо утверждение 2. Но для этого скорее всего надо будет знать, что утверждение 1 справедливо, а этого-то мы еще и не доказали. 4

Метод индуктивных утверждений Фактически нужно показать, что при любом попадании в точку 2 из точки 1 (не только в первый момент) будет справедливо утверждение 2. Но для этого скорее всего надо будет знать, что утверждение 1 справедливо, а этого-то мы еще и не доказали. 5

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

Метод индуктивных утверждений Определение 1. Пусть А – некоторое утверждение, описывающее предполагаемые свойства данных в программе (блок-схеме), а С – утверждение, описывающее то, что мы по предположению должны получить в результате процесса выполнения программы (т. е. утверждение о правильности). Будем говорить, что программа частично правильна (по отношению к А и С), если при каждом выполнении ее с данными, удовлетворяющими предположению А, будет справедливо утверждение С при условии, что программа закончится. Другими словами, если выполнять программу с данными, удовлетворяющими А, то либо она не заканчивается, либо заканчивается и удовлетворяется утверждение С. 7

Метод индуктивных утверждений Таким образом, программа может быть частично правильна, даже если она не заканчивается при некоторых (или всех) входных данных, удовлетворяющих А. Необходимо только, чтобы, если уж программа заканчивается, было справедливо утверждение С с данными, удовлетворяющими А. Определение 2. Будем называть программу (блок- схему) полностью правильной (по отношению к А и С), если она частично правильна (по отношению к А и С) и заканчивается при всех данных, удовлетворяющих А. 8

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

Метод индуктивных утверждений Описание метода индуктивных утверждений Для каждого пути в программе, ведущего из точки I, связан- ной с утверждением А I, в точку J, связанную с утверждением A J (при условии, что на этом пути нет точек с какими-либо допол- нительными утверждениями), докажем, что если мы попали в точку I и справедливо утверждение А I, а затем прошли от точки I до точки J, то при попадании в точку J будет справедливо утвер- ждение A J. Для циклов точки I и J могут быть одной и той же точкой. Чтобы убедиться, что таким способом мы действительно доказываем частичную правильность программы, докажем следующую теорему. Теорема 1. Если можно выполнить все действия, предусмот- ренные описанным методом индуктивных утверждений для некоторой программы, то эта программа частично правильна (относительно А и С). 10

Метод индуктивных утверждений Доказательство. Предположим, что мы выполнили доказательство правильности методом индуктивных утверждений. Начнем выполнять программу с начальными данными, удовлетворяющими допущению А. Нам нужно доказать, что если выполнение программы закончится, то утверждение С будет справедливо, но фактически мы докажем нечто более общее. Мы покажем, что каждый раз, когда мы попадаем в некоторую точку программы, с которой связано определен­ное утверждение, данное утверждение будет справедливым. Это, в частности, предполагает, что, если мы достигнем, последней точки программы (т. е. программа закончится), утверждение С будет справедливо. Доказательство проведем с помощью индукции по N –числу точек программы, через которые мы уже прошли (учитыва- ются точки, связанные с некоторыми утверждениями). 11

Метод индуктивных утверждений 1. Предположим, что в процессе выполнения программы мы попали в первую из этих точек (N = 1). Нужно показать, что связанное с этой точкой утверждение справедливо. Но первая точка – это начальная точка программы, и с ней связано исходное допущение А. Мы знаем, что оно справедливо, ибо речь идет о выполнении программы с такими начальными данными, для которых оно выполняется. 2. Предположим, что мы дошли до некоторой точки (N-й), с которой связано утверждение. Допустим, что это утверждение справедливо (гипотеза индукции). Нужно показать, что если выполнение продолжается и мы попадаем из N-й точки в (N+1)-ю, то связанное с ней утверждение будет также верным. 12

Метод индуктивных утверждений Очевидно, что между N-й и (N+1)-й точками существует некоторый путь. Так как речь идет о методе индуктивных утверждений, то, следовательно, мы уже рассматривали этот путь и показали, что если находимся в N-й точке со справедливым утверждением, а затем проходим из N-й в (N+1)-ю точку, то при ее достижении будет справедливо утверждение. Из этого факта вместе с гипотезой о справедливости утверждения следует, что при попадании в (N+1)-ю точку справедливо утверждение, т. е. то, что требовалось доказать. 13

Метод индуктивных утверждений Таким образом, мы доказали по индукции, что если программа удовлетворяет условиям метода индуктивных утверждений, то при достижении любой из точек программы, с которыми связаны определенные утверждения, соответст­вующие утверждения будут справедливы. Следовательно, если будет достигнута конечная точка программы, то будет справедливо утверждение о правильности, связанное с этой точкой, т. е. рассматриваемая программа является частично правильной. 14

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

Метод индуктивных утверждений ПРИМЕР 7. Требуется доказать, что приведенная на рисунке блок-схема устанавливает переменную XLGST равной макси- мальному значению в массиве X. Замкнутые пути в блок-схеме: 1)1 – 2 2)2 – 3 3) ) ) )2-8 16

Метод индуктивных утверждений Указанные на блок-схеме утверждения – индуктивные утверждения, необходимые для доказательства частичной правильности программы. Так как все эти утверждения имеют аналогичную форму и начинаются с фразы: «При достижении этой точки справедливо…», то это начало фразы мы опускаем. Утверждение о конечности программы мы не помещаем на блок-схеме, поскольку доказатель- ство этого утверждения проводится отдельно от доказательства частичной правильности. Для доказательства частичной правильности нужно исследовать все пути программы. Рассмотрим их по порядку. 17

Метод индуктивных утверждений 1. Путь из точки 1 в точку 2. Предположим, что мы находимся в точке 1 и связанное с ней утверждение справедливо, т. е. данные удовлетворяют исходному допущению. Перейдем из точки 1 в точку 2. Нужно показать, что после прихода в точку 2 связанное с этой точкой утверждение будет справедливо. Если мы попали в точку 2 из точки 1, то имеем I= 1 и XLGST = X 1,1. Так как M 1, то очевидно, что 1 I=1 M+1. Поскольку XLGST = X 1,1 и I=1, то утверждение о XLGST справедливо. 2. Путь из точки 2 в точку 3. Предположим, что мы находимся в точке 2 и справедливо связанное с нею утверждение. Перейдем из точки 2 в точку 3. Требуется показать, что при попадании в точку 3 будет справед- ливо утверждение, связанное с этой точкой. 18

Метод индуктивных утверждений Если мы дошли до точки 3 (из точки 2), то имеем J = 1, а значение XLGST осталось неизменным. Так как N 1, 1 J=1 N+1, а значение I после точки 2 не изменялось, то 1 I M + 1. Однако если мы пришли из точки 2 в точку 3, то известно, что проверка 1 M была истинной, и, комбинируя это отношение с 1 I M + 1, получаем 1 I M. Если I = 1и J = 1, то из утверждения 2 получим XLGST = X 1,J. В противном случае (т.е. при I 1) из утверждения 2 получаем, что XLGST равно максимальному из значений элементов в первых I–1 строках массива X или, более точно, максимальному из значений элементов в первых I–1 строках и из значений первые J–1 = 1–1 = 0 элементов в 1-й строке. Таким образом, очевидно, что при переходе из точки 2 в точку 3 утверждение, связанное с точкой 3, оказывается справедливым. 19

Метод индуктивных утверждений 3. Путь из точки 3 через точки 4, 5 к точке 3. Предположим, что мы находимся в точке 3 и справедливо утверж­дение, связанное с этой точкой. Пройдем через точки 4, 5 к точке 3. Нужно показать, что при возврате в точку 3 соответствующее утверждение останется справед- ливым. Пусть I и J в исходном положении в точке 3 прини- мают значения I N и J N. Мы имеем 1 I N M и 1 J N N+1. При возврате в точку 3 через точки 4 и 5 получим I N+1 = I N и J N+1 = J N + 1. Следовательно, опять имеем 1 I N+1 = I N M. Если мы проходим по этому пути, то проверка J N N была истинной. Из этого, а также из соотношения 1 J N N+1 получаем 1 J N N. Таким образом, при возврате в точку 3 снова имеем 1 < 2 J N+1 = J N + 1 N+1. 20

Метод индуктивных утверждений На всем пути перехода в точку 3 значение XLGST не изменялось, и известно, кроме того, что истинна проверка XLGST. Если учесть истинность утверждения о XLGST до «прохода» по указанному пути, то данное утверждение остается истинным и при возврате в точку 3 с I N+1 = I N и J N+1 = J N + 1. Так как XLGST, то неизменное значение XLGST снова будет максимальным из значений элементов в первых I N+1 – 1 = I N – 1 строках и из значений первых J N+1 – 1 = (J N + 1) – 1 = J N элементов в I N -й строке массива X. 21

Метод индуктивных утверждений 4. Путь из точки 3 через точки 4, 6 в точку 3. Рассуждения для этого пути аналогичны приведенным для предыдущего пути, за исключением того, что при возврате в точку 3 XLGST будет иметь значения. Кроме того, так как выбран этот путь, проверка XLGST была ложной и, следовательно, XLGST

Метод индуктивных утверждений 5. Путь из точки 3 через точку 7 в точку 2. Предполо­жим, что мы находимся в точке 3 и справед- ливо соответствующее утверждение. Перейдем из точки 3 через точку 7 в точку 2. Нужно показать, что при возврате в точку 2 будет справедливо связанное с нею утверждение. Из точки 3 в точку 7 мы попадем только тогда, когда ложна проверка J N. Но из утверждения, относящегося к точке 3, известно, что 1 J N+1. Отсюда можно заключить, что J = N+1. Пусть I в точке 3 принимает значение I N. Утверждение в точке 3 гласит: 1 I N M и XLGST равно максимальному из значений элементов в первых I N – 1 строках и первых J – 1 = (N +1) – 1 = N элементов в I N -й строке массива X. 23

Метод индуктивных утверждений Но так как в массиве X существует только N столбцов, то XLGST равно максимальному из значений элементов в I N строках массива X. Значение XLGST между точками 3 и 2 не изменялось, а значение I изменилось и стало равным I + 1. Так как в точке 3 было справедливо отношение 1 I N M, то это означает, что 1 < 2 I N+1 = I N + 1 M + 1 справедливо в точке 2. Следовательно, при достижении точки 2 будет справедливо утверждение: XLGST равно максимальному из значений элементов в первых I – 1 = (I N + 1) – 1 = I N строках массива X. 24

Метод индуктивных утверждений 6. Путь от точки 2 в точку 8. Предположим, что мы находимся в точке 2, справедливо соответствующее утверждение и мы переходим в точку 8. Необходимо показать, что при достижении точки 8 будет справед- ливо связанное с нею утверждение. Из точки 2 мы перейдем в точку 8, если была ложной проверка 1 M. Но в точке 2 было справедливо неравенство 1 I M+ 1; т.е., можно заключить, что I= M+1. Значение XLGST при переходе из 2 в 8 не изменялось, и, таким образом, из утверждения, относящегося к точке 2, можно заключить, что при попадании в точку 8 XLGST равно максимальному из значений эле­ментов в первых I – 1 = (M + 1) – 1 = M строках массива X. Но массив X содержит только M строк; т.е., XLGST равно максимальному из значений элементов X. 25

Метод индуктивных утверждений Таким образом, мы доказали частичную правильность нашей программы. Нам еще осталось удостовериться, что программа закончится. Отметим, что единственны- ми местами в программе, где изменяются I и J, являют- ся «изолированные» части двух итерационных блоков, управляющие увеличением параметра цикла. Так как значение J увеличивается на 1, а значение N при выполнении внутреннего цикла не изменяется (путь через точки 3, 4, 5, 3 или через точки 3, 4, 6, 3), то значение J должно в конце концов превысить значение N. Таким образом, попадая в точку 3, мы когда-нибудь (после конечного числа выполнений внутреннего цикла) должны попасть в точку 7, а затем в точку 2. 26

Метод индуктивных утверждений При каждом попадании в точку 2 мы затем попадем либо в точку 8 и процесс закончится, либо в точку 3. Если мы попали в точку 3, мы только что видели, как в конце концов дойдем до точки 7 и вернемся в точку 2. При этом значение I будет увеличиваться на 1, а значение M останется неизменным. Следовательно, после конечного числа шагов значение I станет больше значения M. В этот момент мы перейдем из точки 2 в точку 8, и программа закончится. Таким образом, мы доказали конечность нашей программы. Если это доказательство объединить с предыдущим доказательством частичной правильности, то отсюда следует полная правильность программы. 27

Метод индуктивных утверждений ПРИМЕР 8. Требуется доказать, что после завершения программы массив X будет упорядочен 28

Метод индуктивных утверждений ПРИМЕР 8. Требуется доказать, что после заверше- ния программы массив X будет упорядочен (т. е. его элементы будут размещены в неубывающем порядке). Сначала докажем частичную правильность блок-схемы. Для этого исследуем такие пути: 1. Путь от точки 1 к точке 2. Можно легко удостовериться, что если мы находимся в точке 1 и справедливо соответствующее утверждение, а затем проходим из точки 1 в точку 2, то утверждение, относящееся к этой точке, будет справедливо. Когда мы попадем в точку 2, будем иметь I = 2, и, следовательно, истинно 2 I N+1, т.е. утверждение, касающееся X, тривиально, ибо I – 1 = 1. 29

Метод индуктивных утверждений 2. Путь из точки 2 в точку 3. Если мы находимся в точке 2 и верно соответствующее утверждение, а затем пере­ходим из точки 2 в точку 3, то можно легко убедиться, что утверждение 3 будет справедливо. Действительно, при движении из точки 2 в точку 3 выполняются только присваивания Y = X 1 и J = I – 1. Сам массив остается без изменений, и, следовательно, утверждение, касающееся X, продолжает быть справедливым и при достижении точки 3. В этой точке нужно только проверить, что справедлива первая из двух альтернатив, относящихся к массиву X. Таким образом, если мы прошли от точки 2 к точке J, то известно, что 1 N, и вместе с 2 I N + L это показывает, что в точке истинно отношение 1 I N. 30

Метод индуктивных утверждений 3. Путь от точки 3 через точки 4, 5 в точку 3. Предположим, что мы находимся в точке 3, справед- ливо соответствующее утверждение, проходим через точки 4 и 5 и возвращаемся в точку 3. Пусть I и J в точке 3 до прохода по нашему пути имели значения I N и J N. Таким образом, 2 I N и либо J N = I N – 1 и X 1..., = Y,..., X N, либо 2 J N J N – 2 и X 1... … … X N. Если мы прошли по этому пути, отношение J N 1 истинно, и, следовательно, 0 J N+1 < J N – 1. При возвращении в точку 3 I N+1 = I N (не изменяется) и J N+1 = J N – 1. 31

Метод индуктивных утверждений Будут сохраняться соотношения 2 I N+1 = I N N и 0 J N+1 = J N – 1 I N – 2 (вне зависимости от того, какая из альтернатив была справедлива до прохода по указанному пути). Мы знаем, что Y < и массив X уже изменен: на место помещен элемент. Таким образом, при возврате в точку 3 имеет 2 I N+1 = I N N и 0 J N+1 = J N – 1 I N – 2 = I N+1 – 2 и X 1... … X 1 … X N. (вне зависимости от того, какая из двух альтернатив была справедлива до прохода по пути). 32

33 4. Путь из точки 3 через точку 6 в точку 7. Предположим, что мы находимся в точке 3 и справедливо соответствующее утверждение. Перейдем из точки 3 через точку 6 в точку 7. Бели мы двигались по этому пути, то проверка J 1 была ложной, и, следовательно, J < 1. Вместе с утверж­дением в точке 3 это свидетельствует о том, что J = 0. Следовательно, должна быть справедлива вторая альтернатива утвержде- ния в точке 3, так как если 2 I N и J = I – 1, то 1 J, что противоречит утверждению J = 0. Из справедливости второй альтернативы в точке 3 и из равенства J = 0 вытекает, что справедлива вторая альтернатива в точке 7. Вторая альтерна- тива с J = 0 такова: 0 J = 0 I– 2 и... X 1 …X N. Утверждение, что Y каждого из X 1 … X J, тривиально при условии J = 0, так как таких элементов просто нет. Метод индуктивных утверждений

34 5. Путь из точки 3 через точку 4 в точку 7. Предположим, что мы находимся в точке 3 и справедливо соответствующее утверждение. Пройдем из точки 3 в точку 7 через точку 4. Если мы прошли по этому пути, следовательно, проверка Y < X J была ложной, т.е. X J Y. При прохождении по пути ни одна переменная не изменялась. Таким образом, легко видеть, что каждая альтернатива утверждения в точке 3 подразумевает соответствующую альтернативу утверждения в точке 7 (так как X J Y). Метод индуктивных утверждений

35 Метод индуктивных утверждений 6. Путь из точки 7 в точку 8. Очевидно, что справедливость любой части утверждения в точке 7 вместе с присваиванием X J+1 значения Y приводит к справедливости утверждений, относящегося к точке Путь из точки 8 в точку 2. Предположим, что мы находимся в точке 8 и справедливо соответствующее утверждение. Пройдем из точки 8 в точку 2. Пусть I в точке 8 принимает значение I N. Тогда 2 I N N и X 1 … X I … X N. Упорядочены Не упорядочены В точке 2 имеем I N = I N + 1, следовательно, 2 < 3 I N = I N + 1 N+1 и X 1 … … X N. Упорядочены Не упорядочены

36 Метод индуктивных утверждений 8. Путь из точки 2 в точку 9. Если мы проходим по этому пути, следовательно, проверка I N была ложной и N < I. Вместе с 2 I N + 1 это означает, что I = N + 1. Но ут­ верждение, касающееся массива X, в точке 2 при I = N + 1 совпадает с утверждением в точке 9. Таким образом, мы доказали частичную правильность нашей программы. Для доказательства полной правильности нужно показать, что выполнение программы когда-нибудь закончится. Так как при прохождении внешнего цикла значение N не изменяется, а значение I увеличивается и поэтому в конце концов станет больше N при попадании в точку 2, а значение J при прохождении внутреннего цикла уменьшается и, следовательно, в конце концов станет меньше 1 при попадании в точку 3, то все это вместе гарантирует конечность нашей программы.

37 Метод индуктивных утверждений В приведенном доказательстве не учитывается одна важная деталь. Мы показали, что когда-нибудь попадем в точку 9 и при этом будем иметь X 1 Х 2... X N. Но в действительности нам нужно было бы доказать не только это, но и то, что при попадании в точку 9 значения X 1, Х 2,..., X N представляют собой некоторую перестановку из первоначальных значений. Другими словами, исходное множество значений, образующих вектор, лишь переупорядочивается (и множество значений не изменяется). Мы не стали этого доказывать, чтобы не увеличивать объем доказательства и сохранить его обозримость. Однако желающие могут сами убедиться в правоте этого высказывания (и, если необходимо, фор­ мально это доказать).

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

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

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