Теория вычислительных процессов Лекция 2 Доказательство правильности блок-схем Преподаватель: Веретельникова Евгения Леонидовна 1
Доказательство правильности блок-схем ВВЕДЕНИЕ При составлении программы для вычислительной машины мы стремимся к тому, чтобы программа решала некоторую определенную задачу. Однако большинство наших программ содержит ошибки и мы тратим много времени на тестирование и отладку созданных нами неправильных программ. Даже закончив тестирование и отладку программы, мы не можем быть уверены, что она совершенно правильна. Все, что можно сказать о ней, это то, что программа дает правильные результаты для тех частных данных, которые использовались при ее тестировании. Позже, когда программа будет работать с новыми исходными данными, могут обнаружиться и другие ошибки. Каждый опытный программист знает, что программа в течение долгого периода может работать без ошибок, кажется совершенно правильной, и вдруг внезапно, таинственным образом появляется очередная ошибка. Поэтому независимо от интенсивности тестирования никогда нельзя поручиться за правильность программы. 2
Доказательство правильности блок-схем Было бы идеально, если бы мы могли доказать правильность программы, а не ссылаться только на проведенное тестирование. Конечно, если даже удастся доказать, что программа правильна, то нельзя быть в этом абсолютно уверенным. В доказательстве, как и в программе, также могут быть ошибки. Тем не менее, усилия, затраченные на доказательство правильности программы, способствуют всестороннему пониманию программы. Ведь чтобы доказать, что программа правильна, надо очень хорошо в ней разобраться. Опыт показывает, что именно поэтому доказательство правильности весьма полезно и способствует обнаружению тех ошибок, которые могли быть пропущены, если бы доказательство не проводилось. 3
Доказательство правильности блок-схем Если бы можно было формализовать доказательство правильности и проводить его абсолютно надежным образом (автоматически доказывающим устройством), то ему можно было бы полностью доверять. В будущем это, возможно, окажется реальным, но не сейчас. Мы рассмотрим лишь неформально построенные доказательства правильности. Опыт проведения таких доказательств показывает, что при этом возрастают наша уверенность в программе и ее понимание, и поэтому доказательства следует выполнять, хотя они и не приводят к полной гарантии от ошибок. Неформальное доказательство правильности можно рассматривать как некоторую форму систематической проверки программы за столом, без машины, т. е. того, что всегда делает хороший программист. В этой главе даны основные идеи такого доказательства правильности для программ, представленных блок-схемами. 4
Основные принципы доказательства правильности для блок-схем Если мы хотим доказать, что некоторая программа правильна или верна, то прежде всего должны уметь описать то, что по предположению делает эта программа. Назовем такое описание высказыванием о правильности или просто утверждением. В этом случае доказательство правильности состоит из доказательства того, что программа, будучи запущенной, в конце концов окончится (выполнится оператор STOP), и после окончания программы будет справедливо утверждение о правильности. Часто требуется, чтобы программа работала правильно только при определенных значениях входных данных. В этом случае доказательство правильности состоит из доказательства того, что если программа выполняется при соответствующих входных данных, то она когда-либо закончится, и после этого будет справедливо утверждение о правильности. Проиллюстрируем эти идеи на примере доказательства правильности для блок-схемы очень простой программы. 5
Основные принципы доказательства правильности для блок-схем ПРИМЕР 1. Предположим, что нужно вычислить произведение двух любых целых чисел M, N, причем M 0 и опера- цию умножения использовать нельзя. Для этого можно использовать операцию сложения и вычислить сумму из M слагаемых (каждое равно N). В результате получим M N. Рассмотрим блок-схему, реализующую такое вычисление. Нужно доказать, что приведенная прог- рамма правильно вычисляет произведе- ние двух любых целых чисел M и N при условии M 0, т. е. если программа выполняется с целыми числами M и N, где M 0, то она в конце концов окончится (достигнув точки 5) со значением J=M N. 6
Основные принципы доказательства правильности для блок-схем Чтобы удостовериться в правильности работы блок-схемы, можно было бы проверить ее с некоторыми фиксированными данными. Например, давайте «вручную» промоделируем выполнение программы с числами M = 3 и N = 5. Ниже приведены значения переменных I и J в моменты достижения точки 2 на блок-схеме (вход в цикл): Число проходов n через точку 2 Значение I Значение J при выполнении блок-схемы Когда мы в четвертый раз дойдем до точки 2, значение I будет равно 3, т.е. равно M, поэтому выполнение цикла закончится и мы попадем в точку 5. 7
Основные принципы доказательства правильности для блок-схем При попадании в точку 5 переменная J=15=3 5. Таким образом, мы убеждаемся, что при M=3 и N=5 блок-схема работает верно. Хотя это, конечно, и укрепляет нашу уверенность в правильности работы программы, но тем не менее никак не доказывает, что программа будет работать правильно при всех возможных значениях M и N. Можно продолжать проверять программу с другими значениями M и N. Если для некоторых значений M и N будет получен неверный ответ, то надо еще узнать, что он неверен. Однако, если мы даже будем продолжать получать правильные ответы, все равно не будем уверены, что такие ответы будут получаться для любых возможных значений M и N. Всегда остается бесконечное число возможных значений, для которых программа еще не проверялась. 8
Основные принципы доказательства правильности для блок-схем Конечно, если речь идет о некоторой конкретной машине, то значение M и N ограничены некоторым конечным интервалом для целых чисел. В принципе в этом случае можно провести исчерпывающую проверку с числами в этом интервале. Однако для большинства машин этот интервал настолько велик, что проводить исчерпывающую проверку было бы не практично. Кроме того, мы составляем программу обычно таким образом, чтобы она работала верно независимо от размеров N и M. Следовательно, мы будем удовлетворены лишь тогда, когда сможем показать, что программа работает правильно независимо от размеров M и N. Методом тестирования мы этого никогда не достигнем. 9
Основные принципы доказательства правильности для блок-схем Предположим, что вместо выполнения программы с конкрет- ными значениями M и N мы начнем ее выполнять с символи- ческими данными M и N. В этом случае мы получим следующую «трассу» для значений I и J при проходах через точку 2: Число проходов Значение I Значение J через точку N 322 N 433 N... M+1MM N 10
Основные принципы доказательства правильности для блок-схем Видно, что при выполнении цикла M раз (т. е. при M+1-ом попадании в точку 2) I = M, a J = M N. Так как I=M, то мы покидаем цикл и попадаем в точку 5. Таким образом, при достижении точки 5 работа программы заканчивается и мы получаем J = M N. Это показывает, что программа правильно работает для любых значений M и N. Однако отметим, что наша трассировка пред- полагает, что M 0, и поэтому значение I в конце станет равным M (оно начинается с 0 и увеличивается на 1 при каждом прохожде- нии цикла). Если M < 0, то цикл будет повторяться, а значение I никогда не станет равным M; следовательно, программа не сможет закончиться. Таким образом, блок-схема в действительности ра- ботает правильно только для M 0. При любых целых значениях M и N и при условии M 0, как это видно из проведенной трассировки, работа блок-схемы закончится с J = M N. 11
Основные принципы доказательства правильности для блок-схем Кроме того, в таблице есть «пробел» (многоточие). Как определить, какие значения I и J должны стоять в таблице после этого пробела? И как мы можем быть уверены, что они именно такие? На первый вопрос можно ответить следующим образом: прослеживая работу по блок-схеме и заполняя первую часть таблицы, мы начинаем понимать, как изменяются значения I и J при каждом проходе через цикл (у нас есть «образ» этого изменения), и пользуемся этим пониманием для предсказания значений I и J в момент M+1-го попадания в точку 2. Что касается второго вопроса, то для полной уверенности тре- буется провести доказательство. Из таблицы следует, что всякий раз, когда мы попадаем в точку 2, имеем J = I N. Попробуем дока- зать это методом индукции по N – числу проходов через точку 2 12
Основные принципы доказательства правильности для блок-схем 1. При первом попадании (N = 1) в точку 2 (сюда мы приходим из точки 7) имеем I = 0 и J=0. Утверждение J = I N = 0 N = 0, таким образом, справедливо. 2. Предположим, что J = I N справедливо при N-ом попадании в точку 2. Нужно показать, что если мы попадем в точку 2 в N+1-й раз, то утверждение J=I N опять будет справедливо. Пусть I и J при N-ом проходе через точку 2 принимают значения I N и J N. Тогда гипотеза индукции есть J N =I N N. Единственный способ вновь попасть в точку 2 – выполнить тело цикла (точнее, пройти «по петле»), пройдя через точки 3, 4 и возвратясь опять в точку 2. Если это именно так, то, однажды проследив выполнение тела цикла, мы видим, что при возвращении в точку 2 новое значение I равно предыдущему значению плюс 1, а новое значение J – предыдущему значению плюс N. 13
Основные принципы доказательства правильности для блок-схем Таким образом, I N+1 = I N + 1 и J N+1 = J N + N, J N+1 = I N N + N = (I N + 1) N = I N+1 N. (По гипотезе индукции) Следовательно, если мы вновь попадем в точку 2 в N+1-й раз, то J = I N. Доказательство по индукции на этом заканчивается, и мы видим, что при любом попадании в точку 2 справедливо утверждение J = I N. Единственный способ закончить выполнение программы (перестать выполнять тело цикла) – попасть в точку 2 при справедливом условии I = M. В этот момент J = I N = M N, так как I = M. Далее мы попадем в точку 5, и работа заканчивается с J = M N. 14
Основные принципы доказательства правильности для блок-схем Отметим, однако, следующее: мы еще не показали, что выполнение действительно закончится. Мы доказали только, что при каждом попадании в точку 2 справедливо утверждение J = I N, и если выполнение когда-либо закончится, то J = M N. Точнее, доказательство того, что J = I N при каждом проходе через точку 2 не зависит от того, будет ли M 0 или нет. Следовательно, даже если M < 0, то доказательство останется корректным и подтверждает справедливость утверждения J=I N при каждом попадании в точку 2. Но если M < 0, то цикл выполняется «бесконечно», так как I никогда не достигает значения M. Таким образом, выполнение программы никогда не закончится, и значение J = MN нельзя вычислить прави- льно. Однако даже в этом случае всякий раз при достижении точки 2 будет справедливо утверждение J=I N (если это не так, то наше предыдущее доказательство неверно). Справедливость этого можно проверить, проследив за работой программы с каким-нибудь значе- нием M < 0: работа не кончается, но утверждение J = I N в точке 2 всегда будет справедливым. 15
Основные принципы доказательства правильности для блок-схем Следовательно, необходимо еще доказать, что выполнение про- граммы закончится. Для этого следует предположить, что M 0. Итак, надо доказать, что если M 0, то в конце концов при выполнении программы мы попадем в точку 2 с I=M. Это утверждение очевидно: оно следует из блок-схемы программы. Действительно, в начале работы I присваивается значение 0, а затем при каждом проходе через цикл значение увеличивается на 1. Если учесть, что M – целое число и больше или равно 0, то очевидно, что I «дорастет» до M. Однако, чтобы получить более строгое доказательство, используем метод индукции. 16
Основные принципы доказательства правильности для блок-схем Докажем с помощью восходящей индукции по m – переменной, удовлетворяющей условию 0 m M, – что мы когда-нибудь достигнем точки 2 с I=M. 1. При первом попадании в точку 2 имеем I=0, т. е. утверждение справедливо для m=0. Если M=0, то это уже обеспечивает конечный результат. 2. В противном случае предположим, что мы в конце концов попали в точку 2 и I=m при 0 m M. Требуется показать, что мы попадем в точку 2 и с I=m+1. В точке 2 с I=m и 0 m M отношение I = M ложно, так как m < M, и, следовательно, мы пройдем по циклу и вернемся в точку 2. При таком возврате значение I увеличится на 1, т. е. очевидно, что мы попадем в точку 2 со значением I = m + 1, что и требовалось доказать. 17
Основные принципы доказательства правильности для блок-схем Из изложенного выше можно заключить, что если М 0, то в конце концов мы достигнем точки 2 с I=M. В этот момент отношение I=M истинно, и мы попадаем в точку 5, где работа программы заканчивается. Итак, мы доказали (даже слишком подробно), что при выполнении нашей программы с заданными целыми M и N и условием M 0 выполнение ее в конце концов закончится, и при этом мы получим J =M N. 18
Основные принципы доказательства правильности для блок-схем ПРИМЕР 2. Мы провели предыдущее доказательство более подробно, чем это фактически необходимо. Повторим это доказательство, опуская некоторые детали и формальности доказательства по индукции. В частности, доказывая справедливость некоторого высказывания в момент прохож дения через какую-либо из точек внутреннего цикла (как это было в предыдущем примере), мы будем считать, что для этого нужно лишь показать, что: 1)высказывание справедливо при первом попадании в эту точку 2) если мы попали в эту точку и в этот момент высказывание справедливо, а затем выполняется цикл и мы вновь возвращаемся в исходную точку, то высказывание будет вновь справедливо. (Т.Е. проще: выполнение цикла не нарушает истинности высказывания – инварианта цикла.) 19
Основные принципы доказательства правильности для блок-схем Если мы доказали оба этих утверждения, то, восстанавливая необходимые детали, можем доказать с помощью индукции по числу прохождений через точку, что исходное высказыва- ние справедливо при любом попадании в данную точку. Приводя второй вариант этого доказательства правильности, мы будем «приписывать» ключевые утверждения, которые необходимо доказать, непосредственно тем точкам блок- схемы, к которым они относятся. Это поможет яснее представлять нам этапы доказательства правильности. 20
Основные принципы доказательства правильности для блок-схем Докажем теперь, что приведенная на рисунке блок-схема правильна, т. е. если ее начать выполнять с M и N, имеющими некоторые целые значения, причем M 0, то выполнение в конечном итоге закончится с J = M N. 21
Основные принципы доказательства правильности для блок-схем Вначале докажем, что при попадании в точку 2 J=IN. 1. При первом попадании в точку 2 при переходе из точки 1 имеем I=0 и J=0. Таким образом, утверждение J =IN = 0N = 0 справедливо. 2. Предположим, что мы попали в точку 2 и утверждение J = I N справедливо. Пусть I и J в этой точке принимают значения I N и J N, т.е. J N = I N N. Предположим теперь, что мы прошли по циклу (от точки 2 через точки 3, 4 вновь в точку 2). При возвращении в точку 2 I и J принимают новые значения I N+1 и J N+1, которые можно представить следующим образом: I N+1 = I N + 1, J N+1 = I N N+ N = (I N + 1) N = I N+1 N. (Т.к J N = I N N) Итак, при очередном попадании в точку 2 высказывание J=I N вновь справедливо, ЧТД. Т. е. при любом попадании в точку 2 справедливо высказывание J = I N. 22
Основные принципы доказательства правильности для блок-схем Теперь докажем, что в конце концов попадем в точку 2 со значением I=M. При первом попадании в точку 2 имеем I=0. При последующих попаданиях, если таковые есть, I каждый раз увеличивается на 1. Так как значение M нигде в программе не изменяется и мы предположили, что M 0, то очевидно, что в какой-то момент I станет равным M. Если мы попадем в точку 2 при I = M, то будет верно и J = I N = M N. Отношение I = M в этот момент истинно, и мы попадаем по стрелке с пометкой Т (TRUE – истина) в точку 5 с J = M N. На этом доказательство правильности программы заканчивается. 23
Основные принципы доказательства правильности для блок-схем ПРИМЕР 3. Докажем правильность программы вычисления целого частного IQ и остатка IR от деления J1 на J2, где J1 и J2 – любые два целых числа, удовлетворяющие условиям 0 J1 и 1 J2. Операция деления в программе для вычисления IQ и IR не используется. Один из способов указать, что делает программа, – сказать, что она вычисляет два целых числа IQ и IR, таких, что J1 /J2 = IQ + IR/J2 и 0 IR < J2. Это можно записать так: J1 = IQ J2 + IR и 0 IR
25
Основные принципы доказательства правильности для блок-схем Допущения о считываемых значениях для J1 и J2 поставлены непосредственно после ввода. Это указывает на то, что правильность работы программы будет доказываться только для данных, удовлетворяющих этому допущению. Утверждение о правильности блок- схемы связано с ее последней точкой. Кроме того, с начальной точкой цикла связываются два основных факта, которые требуется доказать. Теперь проследим за работой программы с символическими данными для J1 и J2 и выясним, как ведут себя инварианты цикла (основные утверждения о цикле): 26
Основные принципы доказательства правильности для блок-схем Число проходов Значение IQ Значение IR через точку 2 10J1 21J1 – J2 32J1 – 2 J2 43J1 – 3 J Пока IR < J2 Отметим, что при каждом попадании в точку 2 IR = J1 – IQ J2, или J1 = IQ J2 + IR. Это утверждение идентично утверждению о правильности, за исключением того, что последнее еще включает условие 0 IR < J2. Остается показать, что цикл когда-нибудь закончится и при этом будет выполняться условие 0 IR < J2. Высказывания, связанные с точкой 2, утверждают именно эти факты о цикле. 27
Основные принципы доказательства правильности для блок-схем Для доказательства правильности программы сначала покажем, что, как только мы попадем в точку 2, J1 = IQ J2 + JR. 1. При первом проходе через точку 2, двигаясь от точки START к точке 2, имеем IQ = 0 и IR = J1, т. е. утверждение J1 = IQ J2 + IR = = 0 J2 + J1 = J1 справедливо. 2. Предположим, что выполнение программы дошло до точки 2 и справедливо утверждение J1 = IQ J2 + IR. Пусть IQ и IR в этот момент принимают значения IQ N и IR N. Наше справедливое по предположению утверждение записывается: J1 = IQ N J2 + IR N (гипотеза индукции). Пройдем один раз по циклу (от точки 2 через точки 3, 4 опять в точку 2). При возвращении в точку 2 новые значения IQ и IR будут такими: IQ N+1 = IQ N + 1 и IR N+1 = IR N – J2. Таким образом, IQ N+1 J2 + IR N+1 = (IQ N + 1) J2 + (IR N – J2) = IQ N J2 + + J2 + IR N – J2 = IQ N J2 + IR N = J1, (по гипотезе индукции). ЧТД, т. е. при попадании в точку 2 справедливо высказывание J1 =IQ J2 + IR. 28
Основные принципы доказательства правильности для блок-схем Теперь докажем, что в конце концов мы попадем в точку 2 при условии 0 IR < J2. Для этого покажем вначале, что при всяком проходе через точку 2 имеем 0 IR. 1. При первом проходе через точку 2 имеем IR = J1 и по предпо- ложению 0 J1. (Отметим, что это единственное место в доказа- тельстве, где используется данное предположение. Таким образом, если бы мы не потребовали IR 0, то блок-схема должна была бы работать правильно даже для отрицательных значений J1.) 2. Предположим, что мы попали в точку 2 и 0 IR. Пусть в этот момент IR принимает значение IR N. Если мы через цикл вернемся вновь в точку 2, то IR примет новое значение IR N+1 =IR N – J2. Но через цикл мы пройдем только в случае отрицательного ответа на проверку IR N < J2, т. е. если истинно отношение J2 IR N. Но если J2 IR N, то 0 IR N – J2 = IR N+1 истинно. Таким образом, мы доказали, что 0 IR при каждом попадании в точку 2. 29
Основные принципы доказательства правильности для блок-схем Докажем затем, что в конечном итоге мы попадем в точку 2 при справедливом условии IR < J2 (т. е. в этом случае мы будем иметь 0 IR < J2). Отметим, что при каждом проходе через цикл значение IR уменьшается на значение J2. Так как значение J2 в программе нигде не изменяется и так как 1 J2, то, очевидно, при каждом повторении процесса IR уменьшается по крайней мере на 1. Следовательно, в конце концов значение IR должно стать меньше J2 (с помощью метода индукции это можно доказать более строго). 30
Основные принципы доказательства правильности для блок-схем Таким образом, в какой-то момент мы попадем в точку 2 со справедливыми условиями 0 IR < J2 и J1 =IQ J2 + IR. В этот момент условие IR
Основные принципы доказательства правильности для блок-схем ПРИМЕР 6. Во многих примерах мы будем использовать итерационные блоки вида, приведенного на рисунке Предполагается, что действия выполняются в следующем порядке: начальная установка, проверка, тело цикла (если проверка истинна), уве- личение, проверка и т.д. Проверки выполняются сразу же за начальной установкой и после увеличения (этот порядок несколько отличается от по- рядка, принятого в циклах Фортрана). 32 Точка 2, фигурировавшая на всех предыдущих блок-схемах, здесь помещается непосредственно перед проверкой, вслед за начальной установкой и увеличением.
33
Основные принципы доказательства правильности для блок-схем Вначале докажем, что при каждом попадании в точку 2 J =0 и ни один из элементов L 1,..., L I-1 не равен К. 1. При первом попадании в точку2 имеем J=0 и 1 = 1. Утвер- ждение, что ни один из элементов L 1,..., L I-1 = L 0 не равен К, очевидно справедливо, так как элементов вообще еще нет. 2. Предположим, что мы попали в точку 2 и верно утверждение, относящееся к этой точке. Пусть I и J в этот момент принимают значения I N и J N. Таким образом, мы имеем J N = 0 и 1 I N N + 1, и ни один из элементов L 1,..., L N-1 не равен К. Если мы выполняем цикл, т. е. проходим через точки 3, 4 к точке 2, то, вернувшись в точку 2, получаем J N+1 = 0 (так как в цикле значение J не изменялось) и I N+1 = I N
Основные принципы доказательства правильности для блок-схем Если цикл выполняется, то условие I N N было истинным, так же как и 1 I N N + 1; следовательно, 1 I N N. Но при возврате в точку 2 должно выполняться и соотношение 1 < 2 I N + 1 = I N+1 N + 1. Кроме того, мы знаем, что проверка К = дала отрицательный ответ, и, следовательно, ни один из элементов L 1,..., не равен К и элемент также не равен К. Таким образом, при возврате в точку 2 ни один из элементов L 1,...,, не равен К. Следовательно, мы доказали, что при попадании в точку 2 справедливы утверждения J=0, 1 I N+1 и ни один из элементов L 1,..., L I-1 не равен К. 35
Основные принципы доказательства правильности для блок-схем Так как N 1, то очевидно, что по мере проходов по циклу значение I будет возрастать от 1 до N+1. В последний момент проверка I N даст отрицательный результат, и мы попадем в точку 5, а затем в точку 7, с I = N + 1 и J=0. Кроме того, мы знаем, что ни один из элементов L 1,..., L I-1=(N+1)–1=N не равен К. Но существует и еще один возможный путь, ведущий из точки 2 в точку 7, – через точки 3 и 6. Если мы попадем в точку 7 по этому пути, то известно, что J = I 0 (т.к. 1 I N+1), и проверка К = L I оказалась истинной, т. е. L I = L J = К. Однако мы также знаем, что ни один из элементов L 1,..., L I-1=J-1 не был равен К (так как это справедливо в точке 2 и на пути от точки 2 до точки 7 значение I нигде не изменялось). Из этого следует, что в конце концов мы попадем в точку 7, и будет справедливо приведенное утверждение о правильности. 36
Основные принципы доказательства правильности для блок-схем Вывод: алгоритм доказательства 1.Сформулировать и расставить на блок-схеме 4 утверждения: утверждение о входных данных утверждение о правильности инвариант цикла утверждение о конечности 2.Доказать инвариант цикла, используя принцип простой индукции по n – количеству попаданий в точку начала цикла: доказать для первого попадания в данную точку предположить для n-го попадания и доказать для (n+1)-го 3.Доказать, что выполнится утверждение о конечности 4.Показать, что из одновременного выполнения инварианта цикла и утверждения о конечности следует выполнение утверждения о правильности 37