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

Министерство образования Российской Федерации

новосибирский государственный технический университет

___________________________________________________________________________

кафедра автоматики

доказательство правильности программ

Часть 1.

метод индуктивных утверждений

Учебное пособие по курсу «Теория вычислительных процессов и структур»

для студентов специальности 2204

Новосибирск
2002

Глава 1. МАТЕМАТИЧЕСКАЯ ИНДУКЦИЯ

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

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

Простая индукция

1.1. Принцип простой ивдукции

Пусть S(N) — некоторое высказывание о целом числе N и требуется доказать, что S(N) справедливо для всех положи­тельных чисел N.

Согласно простой математической индукции, для этого необходимо

1. Доказать, что справедливо высказывание S(1).

2. Доказать, что если для любого положительного числа N справедливо высказывание S(N), то справедливо и высказы­вание S(N + 1).

Из приведенных выше двух утверждений вытекает, что S(N) справедливо для всех положительных чисел. Этот факт интуитивно очевиден, хотя при аксиоматической трактовке целых чисел сам принцип в такой формулировке следует рассматривать как аксиому. Из первого положения индукции следует, что справедливо S(1), а из второго — что справед­ливо S(2), если справедливо S(1). Но S(1) справедливо, сле­довательно, должно быть справедливо и S(2). Из второго положения индукции вытекает также, что справедливо S(3)> если справедливо S(2). Таким образом, поскольку мы знаем, что S(2) справедливо, то, следовательно, справедливо S(3) и т. д. Отсюда интуитивно видно, что эти два положения вместе доказывают справедливость S(1), S(2), S(3), ..., S(N)....

Рассмотрим пример использования простой индукции.

ПРИМЕР 1. Мы хотим доказать, что для любого поло­жительного числа п сумма первых л положительных целых чисел равна п • (п + 1)/2, т. е.

1+2 + ...+ N=N• (N+1)/2

для любого положительного числа N. Используя простую индукцию, неооходимо только доказать, что

1. «Сумма» верна для N=1, т. е. 1 = 1• (1 + 1)/2. Это очевидно.

2. Если сумма первых п положительных целых чисел равна п • (п + 1)/2, то сумма первых п+L положительных целых чисел равна (п +1) • [(п + 1)+1]/2, т. е. мы предпола­гаем, что формула 1 + 2 + ...+ N = п • (п + 1)/2, справедлива. Это гипотеза индукции. На ее основании мы должны по­пытаться доказать, что справедлива формула

1 + 2 + ...+ N + (п +1) = (п +1) • [(п + 1)+1]/2.

Докажем это следующим образом:

1 + 2 + ...+ N + (п +1) = (1 + 2 + ...+ N )+ (п +1) =

[п • (п + 1)/2] + (п +1) =[(п2 + п)/2] + (п +1) =

(По гипотезе индукции)

[(п2 + п)/2] + [(2п + 2)/2] =( п2 + 3п + 2)/2 =

(п + 1) • (п + 2)/2 = (п +1) • [(п + 1)+1]/2.

Что и требовалось доказать.

Поскольку мы доказали справедливость двух утвержде­ний, то по индукции формула

1 + 2 + ... + п = п • (п + 1)/2

считается справедливой для любого положительного числа п.

1.2. Принцип модифицированной простой индукции

Иногда необходимо доказать, что высказывание S(N) справедливо для всех целых N³N0. Для этого можно довольно легко модифицировать принцип простой индукции. Чтобы доказать, что высказывание S(N) справедливо для всех целых N, необходимо:

1. Доказать, что справедливо S(N0)-

2. Доказать, что если S(N) справедливо для всех целых п³N0, то справедливо и S(N+ 1).

В частности, если требуется доказать справедливость некоторого высказывания S(N) для любых положительных целых п (т. е. для N³0), то необходимо:

1. Доказать, что справедливо S(0).

2. Доказать, что для всех неотрицательных целых п справедливо S(N+1), если справедливо S(N).

ПРИМЕР 2. Для любого неотрицательного числа п доказать, что

20 + 21 + 22 + … + 2N = 2N+1 – 1.

Используя простую индукцию, мы должны

1. Доказать, что 20 = 20+1 – 1 Это очевидно, так как

20 = 1 = 20+1 – 1 = 21 – 1= 2 – 1 = 1.

2. Доказать, что если для всех неотрицательных целых п справедлива формула

20 + 21 + 22 + … + 2N = 2N+1 – 1.

то справедлива и формула

20 + 21 + 22 + … + 2N + 2N+1 = 2(N+1)+1 – 1.

Высказывание 20 + 21 + 22 + ... + 2 N = 2N+1 – 1 называется гипотезой индукции. Второе положение доказывается следующим образом:

20 + 21 + 22 + … + 2N + 2N+1 = (20 + 21 + 22 + … + 2N ) + 2N+1 =

( 2N+1 – 1) + 2N+1 = ( 2N+1 + 2N+1 ) – 1 =

(По гипотезе
индукции)

(2×2N+1 + 2N+1 ) – 1 = 2N+2 – 1 = 2(N+1)+1 – 1.

Иногда нужно доказать справедливость высказывания S(N) для целых п, удовлетворяющих условию п0£п£M0. Так как между п0 и M0 находится конечное число целых чисел, то справедливость S(N) можно доказать простым перебором всех возможных вариантов. Однако легче, а иногда и необходимо (если, например, мы не знаем конкретных значений п0 и M0) доказать S(N) по индукции. В этом случае можно воспользоваться одним из двух вариантов индукции:

Простая нисходящая индукция

1. Доказать, что справедливо S (п0)

2. Доказать, что если справедливо S (п), то для любых целых п0 £п£M0–1 справедливо и S(N + 1).

Простая восходящая индукция

1. Доказать, что справедливо S(M0).

2. Доказать, что если справедливо S(N), то для любых целых п0+1£п£M0 справедливо и S(N – 1).

Интуитивно понятно, что этого достаточно для доказательства справедливости S(N) при любых N, удовлетворяющих условию п0 £п£M0.

1.3. Доказательство высказываний, относящихся
к программам дня вычислительных машин

Иногда не совсем ясно, доказываем ли мы справедливость S(N) для всех N, удовлетворяющих условию п0 £п£M0 или условию п0 £п. В такой ситуации можно добиться успеха, даже и не зная, с каким из случаев имеем дело. Например, при доказательстве правильности программы иногда необхо­димо доказать справедливость некоторого высказывания S в те моменты, когда выполнение программы достигает неко­торой определенной точки. Можно попытаться доказать это методом индукции по п – числу «проходов» через данную точку программы. Однако мы можем и не знать точно, сколько раз проходим через эту точку: это зависит от данных, исполь­зуемых при выполнении программы. Мы можем проходить через нее и конечное (M0), и бесконечное число раз (если программа не заканчивается из-за ошибки). Таким образом, можно попытаться доказать справедливость S(N) для N, удовлетворяющих условию 1£п£M0 или условию 1£п. В любом случае мы можем получить результат, не зная, с каким вариантом мы имеем дело. Мы убеждаемся в справед­ливости S(N) при каждом проходе через определенную точку, если можем:

1. Доказать, что справедливо S(1), т. е. справедливо высказывание S при первом проходе через точку.

2. Доказать, что если справедливо S(N) (т. е. при N-ом проходе через точку), то справедливо и S(N+1), если мы, конечно, попадем в точку в п+1-й раз.

Если мы проходим через точку только т0 раз, то значения N, для которых второе положение, возможно, справедливо, это те значения N, при которых мы п0£п£M0–1. Если же мы проходим через точку бесконечное число раз, то значения N, для которых может быть справедливо второе положение, это значения, удовлетворяющие условию 1£п. Таким образом, если мы докажем оба положения, то тем самым с помощью простой восходящей или простой индукции мы докажем справедливость высказывания S(N) для всех требуемых значений п вне зависимости от того, какой вариант встречается в действительности.

Глава 2. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ
БЛОК-СХЕМ ПРОГРАММ

2.1. Введение

При составлении программы для вычислительной машины мы стремимся к тому, чтобы программа решала некоторую определенную задачу. Однако каждый программист отчетливо и с горечью осознает, что большинство наших программ содержит ошибки. Мы тратим обычно много времени на тестирование и отладку созданных нами неправильных про­грамм. Даже закончив тестирование и отладку программы, мы не можем быть уверены, что она совершенно правильна. Все, что можно сказать о ней, это то, что программа дает правильные результаты для тех частных данных, которые использовались при ее тестировании. Позже, когда программа будет работать с новыми исходными данными, могут обна­ружиться и другие ошибки. Каждый опытный программист знает, что программа в течение долгого периода может рабо­тать без ошибок, кажется совершенно правильной, и вдруг внезапно, таинственным образом появляется очередная ошибка. Поэтому независимо от интенсивности тестиро­вания никогда нельзя поручиться за правильность программы.

Было бы идеально, если бы мы могли доказать правиль­ность программы, а не ссылаться только на проведенное тестирование. Конечно, если даже удастся доказать, что программа правильна, то нельзя быть в этом абсолютно уверенным. В доказательстве, как и в программе, также могут быть ошибки. Тем не менее, усилия, затраченные на доказательство правильности программы, способствуют всестороннему пониманию программы. Ведь чтобы доказать, что программа правильна, надо очень хорошо в ней разо­браться. Опыт показывает, что именно поэтому доказа­тельство правильности весьма полезно и способствует обна­ружению тех ошибок, которые могли быть пропущены, если бы доказательство не проводилось.

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

2.2. Основные принципы доказательства
правильности для блок-схем

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

Проиллюстрируем эти идеи на примере доказательства правильности для блок-схемы очень простой программы.

ПРИМЕР 1. Предположим, что нужно вычислить произ­ведение двух любых целых чисел M, N, причем M³0 и операцию умножения использовать нельзя. Для этого можно использовать операцию сложения и вычислить сумму из M слагаемых (каждое равно N). В результате получим M • N. Рассмотрим блок-схему, реализующую такое вычисление (рис. 2.1). Нужно доказать, что приведенная программа правильно вычисляет произведение двух любых целых чисел M и N при условии M³0, т. е. если программа выполняется с целыми числами M и N, где M³0, то она в конце концов окончится (достигнув точки 5) со значением J=M×N.

Рис. 1

Чтобы удостовериться в правильности работы блок-схемы, можно было бы проверить ее с некоторыми фиксированными данными. Например, давайте «вручную» промоделируем выполнение программы с числами M = 3 и N = 5. Ниже приведены значения переменных I и J в моменты достижения точки 2 на блок-схеме (вход в цикл):

Число проходов п через точку 2 Значение I Значение J

при выполнении блок-схемы

1 0 0

2 1 5

3 2 10

4 3 15

Когда мы в четвертый раз дойдем до точки 2, значение I будет равно 3, т. е. равно M, поэтому выполнение цикла закончится и мы попадем в точку 5.

При попадании в точку 5 переменная J=15=3×5. Таким образом, мы убеждаемся, что при M=3 и N=5 блок-схема работает верно. Хотя это, конечно, и укрепляет нашу уверенность в правильности работы программы, но тем не менее никак не доказывает, что программа будет работать правильно при всех возможных значениях M и N. Можно продолжать проверять программу с другими значениями M и N. Если для некоторых значений M и N будет получен неверный ответ, то надо еще узнать, что он неверен. Однако, если мы даже будем продолжать получать правильные ответы, все равно не будем уверены, что такие ответы будут полу­чаться для любых возможных значений M и N. Всегда остается бесконечное число возможных значений, для которых программа еще не проверялась. Конечно, если речь идет о неко­торой конкретной машине, то значение M и N ограничены некоторым конечным интервалом для целых чисел. В принципе в этом случае можно провести исчерпывающую про­верку с числами в этом интервале. Однако для большинства машин этот интервал настолько велик, что проводить исчер­пывающую проверку было бы не практично. Кроме того, мы составляем программу обычно таким образом, чтобы она работала верно независимо от размеров N и M. Следовательно, мы будем удовлетворены лишь тогда, когда сможем показать, что программа работает правильно независимо от размеров M и N. Методом тестирования мы этого никогда не достигнем.

Предположим, что вместо выполнения программы с конкретными значениями M и N мы начнем ее выполнять с символическими данными M и N. В этом случае мы получим следующую «трассу» для значений I и J при проходах через точку 2:

Число проходов Значение I Значение I

через точку 2

1 0 0

2 1 N

3 2

4 3 3×N

. . .

. . .

. . .

M+1 M M×N

Видно, что при выполнении цикла 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.

Кроме того, отметим, что в таблице есть «пробел» (многоточие). Как определить, какие значения I и J должны стоять в таблице после этого пробела? И как мы можем быть уверены, что они именно такие? На первый вопрос можно ответить следующим образом: прослеживая работу по блок-схеме и заполняя первую часть таблицы, мы начинаем понимать, как изменяются значения I и J при каждом проходе через цикл (у нас есть «образ» этого изменения), и пользуемся этим пониманием для предсказания значений I и J в момент M+1-го попадания в точку 2. Что касается второго вопроса, то для полной уверенности требуется провести доказательство. Из таблицы следует, что всякий раз, когда мы попадаем в точку 2, имеем J = I×N. Попробуем доказать это методом индукции по N – числу проходов через точку 2 (см. главу 1, где имеется исчерпывающее объяснение такого индуктивного доказательства).

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 принимают значения IN и JN. Тогда гипотеза индукции есть JN=IN×N. Единственный способ вновь попасть в точку 2 – выполнить тело цикла (точнее, пройти «по петле»), пройдя через точки 3, 4 и возвратясь опять в точку 2. Если это именно так, то, однажды проследив выполнение тела цикла, мы видим, что при возвращении в точку 2 новое значение I равно предыдущему значению плюс 1, а новое значение J – предыдущему значению плюс N. Таким образом,

IN+1 = IN + 1 и JN+1 = JN + N,

JN+1 = IN×N + N = (IN + 1) × N = IN+1 × N.

(По гипотезе

индукции)

Следовательно, если мы вновь попадем в точку 2 в п N+1-й раз, то J = I×N. Доказательство по индукции на этом заканчивается, и мы видим, что при любом попадании в точку 2 справедливо утверждение J = 1 • N.

Единственный способ закончить выполнение программы (перестать выполнять тело цикла) – попасть в точку 2 при справедливом условии I = M. В этот момент J = I • N = M • N, так как I = M. Дальше мы попадем в точку 5, и работа закан­чивается с J = M×N. Отметим, однако, следующее: мы еще не показали, что выполнение действительно закончится. Мы доказали только, что при каждом попадании в точку 2 справедливо утверждение J = 1 • 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 всегда будет справедливым.

Следовательно, необходимо еще доказать, что выполнение программы закончится. Для этого следует предположить, что M³0. Итак, надо доказать, что если M³0, то в конце концов при выполнении программы мы попадем в точку 2 с I=M. Это утверждение очевидно: оно следует из блок-схемы программы. Действительно, в начале работы I присваивается значение 0, а затем при каждом проходе через цикл значение увеличивается на 1. Если учесть, что M – целое число и больше или равно 0, то очевидно, что I «дорастет» до M. Однако, чтобы получить более строгое доказательство, используем метод индукции.

Докажем с помощью восходящей индукции по 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, что и требовалось доказать.

Из изложенного выше можно заключить, что если М0, то в конце концов мы достигнем точки 2 с I=M. В этот момент отношение I=M истинно, и мы попадаем в точку 5, где работа программы заканчивается.

Итак, мы доказали (даже слишком подробно), что при выполнении нашей программы с заданными целыми M и N и условием M³0 выполнение ее в конце концов закончится, и при этом мы получим J =M • N.

ПРИМЕР 2. Мы провели предыдущее доказательство более подробно, чем это фактически необходимо. Повторим это доказательство, опуская некоторые детали и формаль­ности доказательства по индукции. В частности, доказывая справедливость некоторого высказывания в момент прохож­дения через какую-либо из точек внутреннего цикла (как это было в предыдущем примере), мы будем считать, что для этого нужно лишь показать, что: 1) высказывание справедливо при первом попадании в эту точку, и 2) если мы попали в эту точку и в этот момент высказывание справедливо, а затем выполняется цикл и мы вновь возвращаемся в исходную точку, то высказывание будет вновь справедливо. (то есть проще, выполнение цикла не нарушает истинности высказы­вания – инварианта цикла.) Если мы доказали оба этих утверждения, то, восстанавливая необхо­димые детали, можем доказать с помощью индукции по числу прохождений через точку, что исходное высказывание справедливо при любом попадании в данную точку. Приводя второй вариант этого доказательства правильности, мы будем «приписывать» ключевые утверждения, которые необходимо доказать, непосредственно тем точкам блок-схемы, к которым они относятся. Это поможет яснее представлять нам этапы доказательства правильности.

Докажем теперь, что приведенная на рис. 2.2 блок-схема правильна, т. е. если ее начать выполнять с M и N, имею­щими некоторые целые значения, причем M³0, то выпол­нение в конечном итоге закончится с J = M • N.

Вначале докажем, что при попадании в точку 2 J=I•N.

1. При первом попадании в точку 2 при переходе из точки 1 имеем I=0 и J=0. Таким образом, утверждение J = I•N = 0•N = 0 справедливо.

2. Предположим, что мы попали в точку 2 и утверждение J = I • N справедливо. Пусть I и J в этой точке принимают значения IN и JN, т. е. JN = IN• N. Предположим теперь, что мы прошли по циклу (от точки 2 через точки 3, 4 вновь в точку 2). При возвращении в точку 2 I и J принимают новые значения IN+1 и J N+1, которые можно представить следующим образом:

IN+1 = IN + 1,

J N+1 = IN• N+ N = (IN + 1) • N = IN+1• N.

(Так как JN = IN• N)

Следовательно, при очередном попадании в точку 2 высказы­вание J=I• N вновь справедливо, что и требовалось доказать, т. е. при любом попадании в точку 2 справедливо высказыва­ние J = I • N.

Теперь докажем, что в конце концов попадем в точку 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. На этом доказательство правильности программы заканчивается.

Рис. 2.

ПРИМЕР 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<J2. Как и выше, свяжем непосредственно с блок-схемой программы
(рис. 3) допущения о входных данных и те утверждения, правиль­ность которых требуется доказать.

рис. 3.

Отметим, что допущения о считываемых значениях для J1 и J2 мы поставили непосредственно после ввода. Это ука­зывает на то, что правильность работы программы будет доказываться только для данных, удовлетворяющих этому допущению. Утверждение о правильности блок-схемы связано с ее последней точкой. Кроме того, с начальной точкой цикла связываются два основных факта, которые требуется доказать. Теперь проследим за работой программы с символическими данными для J1 и J2 и выясним, как ведут себя инварианты цикла (основные утверждения о цикле):

Число проходов Значение IQ Значение IR

через точку 2

1 0 J1

2 1 J1 – J2

3 2 J1 – 2 • J2

4 3 J1 – 3 • J2

. . .

. . .

. . Пока IR < J2

Отметим, что при каждом попадании в точку 2

IR = J1 – IQ • J2,

или

J1 = IQ • J2 + IR.

Это утверждение идентично утверждению о правильности, за исключением того, что последнее еще включает условие 0 £ IR < J2. Таким образом, остается лишь показать, что цикл когда-нибудь закончится и при этом будет выполняться условие 0 £ IR < J2. Легко установить, что высказывания, связанные с точкой 2, утверждают именно эти факты о цикле.

Для доказательства правильности программы сначала по­кажем, что, как только мы попадем в точку 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 в этот момент принимают значения IQN и IRN. Наше справедливое по предположению утверждение запи­сывается так: J1 = IQN • J2 + IRN (гипотеза индукции). Пройдем один раз по циклу (от точки 2 через точки 3, 4 опять в точку 2). При возвращении в точку 2 новые значения IQ и IR будут такими: IQN+1 = IQN + L и IRN+1 = IRN – J2. Таким образом,

IQN+1 • J2 + IRN+1 = (IQN + 1) • J2 + (IRN – J2) =

IQN •J2 + J2 + IRN – J2 = IQN •J2 + IRN = J1,

(По гипотезе индукции)

Что и требовалось доказать, т. е. при попадании в точку 2 справедливо высказывание J1 =IQ • J2 + IR.

Теперь докажем, что в конце концов мы попадем в точку 2 при условии 0 £ IR < J2. Для этого покажем вначале, что при всяком проходе через точку 2 имеем 0 £ IR.

1. При первом проходе через точку 2 имеем IR = J1 и по предположению 0 £ J1. (Отметим, что это единственное место в доказательстве, где используется данное предположение. Таким образом, если бы мы не потребовали IR³0, то блок-схема должна была бы работать правильно даже для отрица­тельных значений J1.)

2. Предположим, что мы попали в точку 2 и 0 £ IR. Пусть в этот момент IR принимает значение IRN. Если мы через цикл вернемся вновь в точку 2, то IR примет новое значение IRN+1 =IRN – J2. Но через цикл мы пройдем только в случае отрицательного ответа на проверку IRN < J2, т. е. если истинно отношение J2 £ IRN. Но если J2 £ IRN, то 0 £ IRN – J2 = IRN+1 истинно. Таким образом, мы доказали, что 0 £ IR при каждом попадании в точку 2.

Докажем затем, что в конечном итоге мы попадем в точку 2 при справедливом условии IR < J2 (т. е. в этом случае мы будем иметь 0 £ IR < J2). Отметим, что при каждом про­ходе через цикл значение IR уменьшается на значение J2. Так как значение J2 в программе нигде не изменяется и так как 1 £ J2, то, очевидно, при каждом повторении процесса IR уменьшается по крайней мере на 1. Следовательно, в конце концов значение IR должно стать меньше J2 (с помощью метода индукции это можно доказать более строго).

Таким образом, в какой-то момент мы попадем в точку 2 со справедливыми условиями 0 £ IR < J2 и J1 =IQ • J2 + IR. В этот момент условие IR<J2, естественно, истинно, и из точки 2 мы идем в точку 5, а затем в точку 6. Так как на пути из точки 2 в точку 6 ни одна переменная не изменяется, то очевидно, что в момент прихода в точку 6 утверждение о правильности будет справедливо. Следовательно, мы доказа­ли, что при выполнении программы с целыми J1 и J2, удовлетворяющими условиям 0 £ J1 и 1 £ J2, программа в какой-то момент закончится, и будут справедливы отношения J1 = IQ • J2 + IR и 0£IR<J2, т, е. IQ и IR будут целыми частным и остатком от деления J1 на J2.

2.3. Дополнительные примеры доказательства
правильности блок-схем программ

В этом разделе рассмотрены несколько дополнительных примеров доказательства правильности для блок-схем программ с помощью метода индукции (без некоторых деталей).

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

ПРИМЕР 4. Мы хотим доказать, что приведенная на рис. 4 блок-схема вычисляет и печатает среднее значение и максимальное из всех чисел во входном файле. Сначала докажем, что справедливо утверждение, связанное с точкой 2.

1. Если программа выполняется с входным файлом, со­держащим одно и более вещественных чисел, то можно вы­полнять первый блок (так как входной файл не пуст), и при первом попадании в точку 2 значение N равно 1, а значение XLGST и SUM – первые числа в исходном входном файле. Таким образом, при первом достижении точки 2 утверждения о N, XLGST и SUM справедливы.

Рис. 4

2. Предположим, что мы находимся в точке 2 и утверждения о N, XLGST и SUM справедливы. Нужно показать, что, если мы пройдем по циклу и вернемся в точку 2, эти утверждения будут оставаться верными. Отметим, что при прохождении цикла в X считывается очередное значение из входного файла (файл по определению не пуст, иначе цикл не выполнялся бы), значение N увеличивается на 1, а значение SUM становится SUM + Х. Поэтому при возврате в точку 2 значение N вновь указывает число считанных из входного файла данных (больше предыдущего на 1), а значение SUM вновь будет суммой всех считанных из файла чисел (сумма всех предварительно считанных чисел плюс последнее прочитанное число). Затем при каждом выполнении цикла переменная XLGST (мы предполагаем, что это наибольший из всех считанных элементов) сравнивается с новым элементом, считанным последним в X из файла. Если отношение Х £ XLGST истинно, то по блок-схеме XLGST не изменяется, и это верно, так как ее новое значение представляет собой самое большое число из всех считанных из файла. Если же отношение Х £ XLGST ложно, то последний считанный элемент – самый большой из всех считанных, и поэтому в блок-схеме предусмотрена запись значения X в XLGST. Таким образом, при возврате в точку 2 (пройдем ли мы в нее через точки 2, 3, 4 или через точки 2, 3, 5, 6) XLGST всегда будет наибольшим из всех считанных до этого значений, что и требовалось доказать, т. е. при каждом проходе через точку 2 утверждения, касающиеся N, XLGST и SUM, справедливы.

Ясно, что в конце концов мы попадаем в точку 2, когда во входном файле не останется больше элементов, которые можно было бы прочитать. Это произойдет потому, что при каждом прохождении цикла считывается один очередной элемент файла, а мы (неявно) предполагали, что входной файл содержит конечное число элементов. Следовательно, после конечного числа прохождений через цикл все элементы входного файла будут прочитаны. После этого проверка на конец файла даст ответ ДА, и мы выйдем из цикла, имея следующие значения: N – число элементов чисел, считанных на данный момент; XLGST – наибольший из всех элементов в исходном входном файле; SUM – сумма всех элементов в исходном входном файле.

При попадании в точку 8 переменная AVG будет иметь значение AVG =SUM/N, a XLGST – то же значение, которое указано выше. Таким образом, работа программы в конце концов закончится, и, когда это произойдет, AVG и XLGST будут иметь требуемые значения.

ПРИМЕР 5. Мы хотим доказать, что приведенная на рис. 5 блок-схема обеспечивает правильное вычисление суммы . Сначала покажем, что при каждом попадании в точку 2 выполняются соотношения 1 £ I £ N+1 и .

Рис. 5.

1. При первом попадании в точку 2 имеем I = 1 и SUM =0; следовательно, утверждения, что 1 £ I < N + 1 и SUM = , справедливы.

2. Предположим, что мы находимся в точке 2 и 1 £ I £ N + 1 и SUM= справедливы. Пусть I и SUM в этой точке при нимают значения IN и SUMN, т. е. 1 £ IN £ N + 1 и =. Если мы пройдем по циклу и вернемся в точку 2, то получим IN+1 =IN+ 1 и

SUMN+1 = SUMN ++

=

Кроме того, если цикл повторялся, то проверка IN £ N давала положительный ответ, а так как истинно и утверждение 1 £ IN £ N + 1, то, следовательно, 1 £ IN £ N. Но в этом случае при возврате в точку 2 имеем
1 < 2 £ IN + 1 = IN+1 £ N+ 1. Таким образом, справедливость утверждений
1 £ I £ N + 1 и SUM= при прохождении точки 2 доказана.

Легко видеть, что если 1 £ N, то переменная I, увеличиваясь с 1 каждый раз на 1, в конце концов станет равной N+ 1. В этот момент проверка даст отрицательный ответ и мы попадем в точку 4, где имеем SUM= и I=N+1, или, что тоже самое, SUM = . Таким образом, мы доказали, что работа программы (достигнув точки 4) прекратится и SUM= .

ПРИМЕР 6. Во многих примерах (блок-схема, о которой идет речь в данном примере, показана на рис. 6) мы будем использовать итерационные блоки вида, приведенного на рис. 7. Предполагается, что действия выполняются в сле­дующем порядке: начальная установка, проверка, тело цикла (если проверка истинна), увеличение, проверка и т. д. Проверки выполняются сразу же за начальной установкой и после увеличения (этот порядок несколько отличается от порядка, принятого в циклах Фортрана). Точка 2, фигурировавшая на всех предыдущих блок-схемах, здесь помещается непосредственно перед проверкой, вслед за начальной установкой и увеличением.

Рис. 6.

Рис. 7.

Вначале докажем, что при каждом попадании в точку 2 J =0 и ни один из элементов L1, ..., LI-1 не равен К.

1. При первом попадании в точку2 имеем J=0 и 1 = 1. Утверждение, что ни один из элементов L1, ..., LI-1 = L0 не равен К, очевидно справедливо, так как элементов вообще еще нет.

2. Предположим, что мы попали в точку 2 и верно утверждение, относящееся к этой точке. Пусть I и J в этот момент принимают значения IN и JN. Таким образом, мы имеем JN = 0 и L £ IN £ N + 1, и ни один из элементов L1, ..., LN-1 не равен К. Если мы выполняем цикл, т. е. проходим через точки 3, 4 к точке 2, то, вернувшись в точку 2, получаем JN+1 = 0 (так как в цикле значение J не изменялось) и IN+1 = IN + L. Если цикл выполняется, то условие IN £ N было истинным, так же как и 1 £ IN £ N + 1; следовательно, 1 £ IN £ N. Но при возврате в точку 2 должно выполняться и соотношение 1 < 2 £ IN + 1 = IN+1 £ N + 1. Кроме того, мы знаем, что проверка К = дала отрицательный ответ, и, следовательно, ни один из элементов L1, ..., не равен К и элемент также не равен К. Таким образом, при возврате в точку 2 ни один из элементов L1, ..., , не равен К. Следовательно, мы доказали, что при попадании в точку 2 справедливы утверждения J=0, 1 £ I £ N+1 и ни один из элементов L1, ..., LI-1 не равен К.

Так как N³1, то очевидно, что по мере проходов по циклу значение I будет возрастать от 1 до N+1. В послед­ний момент проверка I £ N даст отрицательный результат, и мы попадем в точку 5, а затем в точку 7, с I = N + 1 и J=0. Кроме того, мы знаем, что ни один из элементов L1, ..., LI-1=(N+1)–1=N не равен К. Но существует и еще один возможный путь, ведущий из точки 2 в точку 7, – через точки 3 и 6. Если мы попадем в точку 7 по этому пути, то известно, что J = I ¹ 0 (так как 1£ I £ N+1), и проверка К = LI оказалась истинной, т. е. LI = LJ = К. Однако мы также знаем, что ни один из элементов L1, ..., LI-1=J-1 не был равен К (так как это справедливо в точке 2 и на пути от точки 2 до точки 7 значение I нигде не изменялось). Из этого следует, что в конце концов мы попадем в точку 7, и будет справедливо приведенное утверждение о правильности.

2.4. Метод индуктивных утверждений

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

Предположим, например, что мы имеем дело с блок-схемой общего вида, приведенной на рис. 8.

Рис. 8.

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

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

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

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

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

Описание метода индуктивных утверждений

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

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

Теорема 1. Если можно выполнить все действия, предусмотренные описанным методом индуктивных утверждений для некоторой программы, то эта программа частично правильна (относительно А и С).

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

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

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

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

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

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

Для доказательства частичной правильности нужно исследовать все пути программы. Рассмотрим их по порядку.

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

2. Путь из точки 2 в точку 3. Предположим, что мы находимся в точке 2 и справедливо связанное с нею утверждение. Перейдем из точки 2 в точку 3. Требуется показать, что при попадании в точку 3 будет справедливо утверждение, связанное с этой точкой. Если мы дошли до точки 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 = X1,J. В противном случае (т. е. при I¹1) из утверждения 2 получаем, что XLGST равно максимальному из значений элементов в первых I–1 строках массива X или, более точно, максимальному из значений элементов в первых I–1 строках и из значений первые J–1 = 1–1 = 0 элементов в 1-й строке. Таким образом, очевидно, что при переходе из точки 2 в точку 3 утверждение, связанное с точкой 3, оказывается справедливым.

Рис. 9.

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

4. Путь из точки 3 через точки 4, 6 в точку 3. Рассужде­ния для этого пути аналогичны приведенным для предыдуще­го пути, за исключением того, что при возврате в точку 3 XLGST будет иметь значения . Кроме того, так как выбран этот путь, проверка £ XLGST была ложной и, следовательно, XLGST < . Таким образом, больше максимального из значений элементов первых IN – 1 строк и JN – 1 элементов в IN-й строке. Отсюда следует, что при возврате в точку 3 значение XLGST остается мак­симальным из значений элементов первых IN+1 – 1 = IN – 1 строк и первых
JN+1 – 1 = (JN + 1) – 1 = JN элементов в IN-й строке массива X.

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

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.

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

ПРИМЕР 8. Требуется доказать, что после завершения программы массив X будет упорядочен (т. е. его элементы будут размещены в неубывающем порядке). Сначала дока­жем частичную правильность блок-схемы
(рис. 10). Для этого исследуем такие пути:

1. Путь от точки 1 к точке 2. можно легко удостовериться, что если мы находимся в точке 1 и спра­ведливо соответствующее утверждение, а затем проходим из точки 1 в точку 2, то утверждение, относящееся к этой точке, будет справедливо. Когда мы попадем в точку 2, будем иметь
I = 2, и, следовательно, истинно 2 £ I £ N+1, т. е. утверждение, касающееся X, тривиально, ибо I – 1 = 1.

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

Рис. 10.

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

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 и £ ... £ X1 … XN. Утверждение, что Y ³ каждого из X1 … XJ, тривиально при условии J = 0, так как таких элементов просто нет.

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

6. Путь из точки 7 в точку 8. Очевидно, что справедли­вость любой части утверждения в точке 7 вместе с присваи­ванием XJ+1 значения Y приводит к справедливости ут­верждений, относящегося к точке 8.

7. Путь из точки 8 в точку 2. Предположим, что мы находимся в точке 8 и справедливо соответствующее утверждение. Пройдем из точки 8 в точку 2. Пусть I в точке 8 принимает значение IN. Тогда 2 £ IN £ N и

X1 £ … £ XI … XN.

Упорядочены Не упорядочены

В точке 2 имеем IN = IN + 1, следовательно, 2 < 3 £ IN = IN + 1 £ N+1 и

X1 £ … £ … XN.

Упорядочены Не упорядочены

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, то все это вместе гаран­тирует конечность нашей программы.

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

2.5. Сокращенные доказательства правильности

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

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

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

3.1. Введение

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

В разд. 3.2 метод проиллюстрирован на простых програм­мах, написанных на Фортране, а в разд. 3.3 —на программах, написанных на ПЛ/1.

3.2. Примеры доказательства правильности программ на фортране

ПРИМЕР 1.

READ (5, 1) J1, J2 (Операторы READ… FORMAT производят ввод

1 FORMAT (2I10) информации по соотвнтствующему формату)

С ЗНАЧЕНИЯ, СЧИТЫВАЕМЫЕ В J1 И J2 –

С ЦЕЛЫЕ, УДОВЛЕТВОРЯЮЩИЕ УСЛОВИЯМ

С 0.LE.J1 И 1.LE.J2. (логические операции: LE – “£” ;

IQ=0 LT – “< “

IR=J1 EQ – “=”

2 IF(IR .LT.J2) GO TO 4 GE – “³”
С J1 .EQ. IQ * I2 + IR AND 0 .LE. IR GT – “>”
IQ=IQ+1 NE – “¹”
IR=IR–J2

3 GO TO 2 (C – признак комментария)

4 WRITE (6,5) IQ, IR (Операторы WRITE … FORMAT производят вывод

5 FORMAT (2I10) информации по соотвнтствующему формату)

С JL .EQ. IQ*J2 + IR AND 0.LE. IR AND
С IR .LT. J2

STOP

END

Приведенная программа на Фортране – это просто некото­рый вариант программы, блок-схема которой приведена на рис. 3. Напомним, что программа вычисляет целое частное IQ и остаток IR от деления целого J1 на целое J2. Мы уже включили в качестве комментариев в программу индуктивные утверждения, необходимые для доказательства частичной правильности. Например, комментарий, помещенный сразу после оператора с меткой 2, нужно рассматривать как коммен­тарий, связанный с точкой, расположенной перед выполня­емой в этом операторе проверкой. Таким образом, предпо­лагается, что в момент прихода в точку, находящуюся непо­средственно перед проверкой в операторе с меткой 2, спра­ведливы утверждения J1 = IQ× J2 + IR и
0 £ IR. Отметим, что в доказательствах мы используем „ = " как символ равенства, а не присваивания.

После этого доказательство частичной правильности данной программы почти идентично доказательству частич­ной правильности для блок-схемы на рис. 3. При этом необходимо рассмотреть следующие пути:

1. Путь от оператора READ до оператора с меткой 2. Предположим, что только что выполнился оператор READ и справедливо утверждение, записанное сразу после него. Теперь последовательно выполняются операторы до опера­тора с меткой 2. Нам нужно показать, что справедливо утверждение, записанное после этого оператора. Если мы дошли до этой точки, то имеем IQ = 0, IR = J1, 0 £ J1 и 1 £ J2. Таким образом,

J1=IQ×J2 + IR=0×J2 + J1=J1

и 0£ J1= IR.

Следовательно, наше утверждение справедливо.

2. Путь от оператора с меткой 2 до оператора с меткой 3 и опять к оператору с меткой 2 (основной цикл программы). Предположим, что мы выполняем оператор 2 (мы перестаем говорить «оператор с меткой 2» и начи­наем употреблять «оператор 2». Здесь уместно отметить, что если убрать из языка программирования метки, то идентифицировать оператор станет весьма затруднительно) и справедливо записанное после него утверждение, затем выполняем цикл и возвращаемся к метке 2. Необходимо показать, что указанное утверждение снова будет справедливо. Пусть IQ и IR до выполнения цикла принимают значения IQN и IRN. Тогда J1 =IQN • J2 + IRN и 0 £ IRN. При возврате к метке 2 после прохождения цикла значения IQ и IR будут
IQN+1 = IQN + 1 и IRN+1 = IRN – J2, а значения J1 и J2 останутся без изменений. Таким образом, после возврата к метке 2 имеем

IQN+1 • J2 + IRN+1 = (IQ + 1)× J2 + (IRN – J2) =

= IQN ×J2 + J2 + IRN – J2 = IQN • J2 + IRN = J1.

Кроме того, известно, что если мы проходили по циклу, то проверка
IRN .LT. J2 дала отрицательный результат, т. е. J2 £ IR. Отсюда следует, что при возврате к метке 2 имеем 0 £ IRN – J2 = IRN+1.

3. Путь от оператора 2 к оператору 4. Предположим, что мы выполнили оператор 2, справедливо соответствующее утверждение и переходим к оператору 4. Нужно показать, что справедливо утверждение, записанное ниже этого опе­ратора. Оператор 2 передаст управление на оператор 4 только при положительном результате проверки IR .LT. J2. При переходе от оператора 2 к оператору4 ни одно из значении переменных не изменяется, и, следовательно, при достижении метки 4 мы имеем J1 = IQ×J2 + IR, 0£IR и, кроме того, IR < J2. Таким образом, мы доказали частичную правильность.

Доказательство конечности программы на Фортране иден­тично доказательству конечности для блок-схем. Для дока­зательства конечности программы необходимо только пока­зать, что при выполнении программы мы в конце концов выйдем из единственного в программе цикла. Следовательно, надо показать, что проверка IR .LT. J2, управляющая циклом, когда-нибудь даст положительный результат. Так как значе­ние IR при каждом прохождении цикла уменьшается на вели­чину J2, a J2 остается без изменений и, кроме того, 1 £ J2, то можно заключить, что IR уменьшается каждый раз по крайней мере на 1 и когда-нибудь станет меньше J2. В этот момент условие IR < J2 станет справедливым и мы выйдем из цикла, т. е. программа закончится.

ПРИМЕР 2.

С1 Х – ВЕЩЕСТВЕННЫЙ МАССИВ, ЕГО РАЗМЕР

С1 N .GE. 2

XSMLST = X(L)

DO 10 I = 2, N

C2 XSMLST РАВНО МИНИМАЛЬНОМУ ИЗ Х(1), ..., Х(I – 1)

С2 КРОМЕ ТОГО, 2 .LE. 1 И I .LE. N

IF (XSMLST .LE. X(I)) GO TO 10

XSMLST = X(I)

C3 XSMLST РАВНО МИНИМАЛЬНОМУ Х(1), ..., X(I – L)

C3 КРОМЕ ТОГО, 3 .LE. 1 И I .LE. N + 1

10 CONTINUE

C4 XSMLST РАВНО МИНИМАЛЬНОМУ ИЗ Х(1),..., X(N)

Предполагается, что приведенный фрагмент программы должен присвоить XSMLST значение наименьшего элемента из массива Х(1), ... , X(N). В Фортране цикл строится по следующей основной схеме:

 

DO метка I = M, N

С ПРИМЕЧАНИЕ 1

Тело цикла

С ПРИМЕЧАНИЕ 2

метка CONTINUE

Рис. 11.

Эта схема работает аналогично приведенной на рис. 11 блок-схеме.

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

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

1. Путь от начала фрагмента до точки 2 (точки, с которой связано утверждение 2). Если мы попадаем в эту точку, то XSMLST = Х(1) и I = 2, и очевидно, что значение XSMLST равно наименьшему из Х(1), ..., Х(I–1) =
= Х(2 – 1) = Х1 и 2 £ I = 2 £ N (так как N ³ 2). (Обратите внимание, что без условия N ³ 2 наше утверждение доказать нельзя, и, следова­тельно, правильная работа программы не гарантируется, если N = 1.)

2. Путь от точки 2 до точки 3 (точки, с которой связано утверждение 3). Предположим, что мы достигли точки 2, утверждение 2 справедливо,
I имеет значение IN и мы проходим по телу цикла, возвращаясь в точку 2. В теле цикла XSMLST сравнивается с Х(IN) и, если XSMLST £ X(IN), XSMLST остается без изменений. В противном случае значение заменяется на Х(IN). Так как до этого известно, что значение XSMLST равно наименьшему из Х(1), ... , Х(IN – 1), то можно легко убедиться, что теперь значение XSMLST будет равно наименьшему из Х(1), ... , Х(IN). Однако, прежде чем мы дойдем до точки 3, значение I увеличится на 1, и, таким образом, IN+1 = IN + 1; следовательно, значение XSMLST снова будет равно наименьшему из Х(1), ... , Х(IN) = Х(IN+1–1). Кроме того, из при­мечания 2 известно, что 2 £ IN £ N, и, следовательно, в точке 3

3 £ IN+1 = IN + 1 £ N + 1.

3. Путь из точки 3 к точке 2. Мы пройдем по этому пути, если только проверка I £ N даст положительный ответ. При этом условии справедливость примечания 3 приводит к справедливости примечания 2 в момент достижения этой точки.

4. Путь из точки 3 в точку 4. Мы пройдем по этому пути, если только проверка 1 £ N даст отрицательный ответ, т. е. при I > N. Но так как справедливо утверждение в примечании 3, следовательно, I = N+1, и при достижении точки 4 значение XSMLST будет равно наименьшему из Х(1), ... , Х(I – 1) =
= X[(N + 1) – 1] = X(N), что и требовалось доказать, т. е. доказана частичная правильность.

Конечность этого фрагмента программы очевидна: здесь есть только один цикл, и он является фортрановским. (Заметим, что конечность фортрановского цикла, если в его теле нет переходов вне цикла, очевидно, следует считать свойством, присущим самому языку).

Эти два примера показывают, что метод индуктивных утверждений можно распространить непосредственно и на дока­зательства правильности программ, написанных на Фортране. Затруднение заключается лишь в том, что управление в про­граммах на Фортране не такое явное, как в блок-схемах. Это приводит к тому, что в программах легко не заметить некоторые пути или неправильно их интерпретировать (например, можно предположить, что в операторе цикла проверка выполняется перед выполнением тела цикла). Кроме того, нужно приписывание индуктивных утверждений к некоторым точкам в программе на Фортране проводить очень внимательно и все время помнить, с какой неявной точкой связано соответ­ствующее утверждение. Например, один-единственный опера­тор Фортрана, такой, как оператор DO, фактически состоит из нескольких действий: установки счетчика, увеличения счетчика и проверки. При доказательстве правильности мы должны четко осознавать, с какой из этих точек связано индуктивное утверж­дение. Использование переходов GO TO в программах на Форт­ране тоже порождает проблемы. Если в программе много пере­ходов и при их использовании не придерживались некоторой дисциплины, то программу часто трудно понимать и трудно доказывать ее правильность. Это объясняется тем, что сложно проследить за всеми возможными путями выполнения про­граммы и указать нужные для этих путей индуктивные утверж­дения. (Однако существует и иная точка зрения Если у нас есть только переходы, то программа на фортране становится полностью аналогичной блок-схеме и доказатель­ство правильности проходит так же легко, как и для блок-схем, ибо мы «видим» все точки с утверждениями. Но переходы действительно усугуб­ляют трудности «неявных» точек, например, в операторе цикла.)

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

ПРИМЕР 3.

С MAIN PROGRAM

.

.

.

С1 0 .LE. I AND 1 .LE. J AND A(I, J)

CALL DIV(I, J, K, L)

С2 0 .LE. I AND 1 .LE. J AND A(I, J)

C2 AND I .EQ. K*J + L AND 0 .LE. L AND I .LT. J

.

.

.

END

.

.

.

SUBROUTINE DIV (JL, 12, IQ, IR)

C3 0 .LE. J1 AND 1.LE. J2

IR = J1

2 IF (IR .LT. J2) GO TO 4

C4 J1.EQ .IQ*J2 + IR AND 0 .LE. IR

IQ = IQ + 1
IR = IR – J2

3 GO TO 2

4 RETURN

C5 J1 .EQ. IQ*J2 + IR AND 0 .LE. IR AND IR .LT. J2

END

В этом примере нас прежде всего будет интересовать, как обрабатывать подпрограммы. Поэтому мы не приводим целиком основную программу, а лишь намечаем некоторую программу, содержащую обращения к подпрограммам. Подпрограмма DIV аналогична программе, приведенной в примере 1, но оформлена как подпрограмма. Она предназначена для вычи­сления целых частного и остатка от деления параметра J1 на параметр J2; полученные значения возвращаются как значения параметров IQ и IR. Доказательство того, что эта подпрограмма верна, аналогично доказательству, приведен­ному в примере 1. Поэтому будем считать, что доказательство правильности этой подпрограммы уже проведено, и докажем, что правильна основная программа. Один из этапов такого доказательства заключается в том, чтобы показать, что если, непосредственно перед обращением к подпрограмме спра­ведливо утверждение С1, а затем мы пройдем эту точку, выполним подпрограмму и вернемся из нее, то будет справед­ливо утверждение С2. Мы считаем, что A(I, J) в примечаниях С1 и С2 — некоторые утверждения, относящиеся к перемен­ным I и J. Чтобы доказать этот факт, мы поступим следую­щим образом. Так как фактические параметры I, J, К, L спомощью механизма обращения сопоставляются с соответст­вующими формальными параметрами J1, J2, IQ, IR, то сначала следует доказать, что из утверждения С1 следует утверждение СЗ в начале подпрограммы; для этого имена параметров J1, J2, IQ и IR в этом утверждении заменяются на имена соответствующих фактических параметров I, J, К, L. Другими словами, нужно доказать, что С1 подразумевает С3', где С3' – утверждение, полученное путем замены в С3 J1 на I, J2 на J, IQ на К и IR на L. Таким образом, нужно показать, что из 0.LE. I, 1.LE. J и A(I, J) следует 0.LE. I и 1.LE. J. Это очевидно. Кроме того, известно, что справедливо и на­чальное допущение о правильности параметров подпро­граммы. Так как мы считаем, что правильность подпрограммы уже доказана, то нам не надо обращать внимание на детали строения этой программы. Мы знаем, что утверждение С5, связанное с точкой, непосредственно предшествующей опера­тору RETURN, будет справедливо и после того, как мы вернемся в основную программу. Конечно, это утверждение относится к формальным параметрам, но оно будет справед­ливо и для фактических параметров после того, как мы вернемся и попадем в точку, с которой связано утверждение С2. Таким образом, для того чтобы убедиться в справедли­вости утверждения С2 при достижении соответствующей точки программы, следует лишь показать, что из С5' следует С2. Утверждение С5' получается из С5 заменой J1 на I, J2 на J, IQ на К и IR на L. Другими словами, из 1 .EQ. К * J + L AND 0 .LE. L AND L .LT. J следует
0 .LT. I AND 1 .LE. J AND A(I, J) AND I .EQ. K*J + L AND 0 .LE. L
AND L.LT. J. легко убедиться, что из С5' не следует целиком все утверждение С2, а следует лишь под­черкнутая часть С2. Как же убедиться, что оставшаяся (невыделенная) часть также справедлива, если мы попадаем в точку, соответствующую С2? Отметим, что эта часть утверж­дения идентична утверждению С2. Следовательно, если мы будем знать, что переменные I и J (в С1 упоминаются только они) в подпрограмме не изменяются, то можно сделать вывод, что из справедливости С1 перед обращением к под­программе следует справедливость соответствующей части С2 после обращения. Так как фактические параметры I, J сопоставляются с формальными параметрами подпрограммы J1, J2, то теперь следует просмотреть подпрограмму: не изменяются ли значения J1 или J2. Студент может легко проверить, что ни J1, ни J2 не изменяются. Отсюда мы делаем вывод, что утверждение 0 .LE. I AND 1 .LE. J AND A(I, J) продолжает оставаться справедливым и в момент достижения точки, связанной с утверждением С2.

Приведенное доказательство иллюстрирует общий метод доказательства для случаев с подпрограммами. Сначала выясняется, что делается в подпрограмме по предположению, и это доказывается обычным методом индуктивных утвержде­ний. Далее при доказательстве правильности программы, обращающейся к этой или еще и другим подпрограммам (если некоторый путь содержит такое обращение), поступаем следующим образом. Сначала доказываем, что при обращении к подпрограмме справедливо утверждение, относящееся к ее началу (здесь описываются допущения, касающиеся значений параметров). В примере мы показывали, что из С1 следует С3'. Затем доказываем, что из утверждения, связанного с оператором возврата (это утверждение о правильности под­программы), следует справедливость всего (или части) утверждения, относящегося к точке (в вызывающей про­грамме), непосредственно следующей за обращением. В примере мы показали, что из С5 следует часть С2. Кроме этого, можно использовать и тот факт, что утвержде­ния, относящиеся к переменным, значения которых не изме­няются в подпрограмме, продолжают оставаться справедли­выми и после возврата из подпрограммы. В примере показано, что из С1 следует оставшаяся часть С2 (С1 – утверждение в вызывающей программе, включающее лишь переменные, значения которых в подпрограмме не изменились).

33. Примеры доказательства правильности программ на пл/1

Как для программ на Фортране, так и для программ на языке ПЛ/1 метод доказательства правильности в принципе один и тот же, однако мы хотели бы показать, как на этом методе отражаются механизмы управления, присущие ПЛ/1.

ПРИМЕР 1

/* Х(1: N) МАССИВ ВЕЩЕСТВЕННЫХ ЗНАЧЕ­НИЙ РАЗМЕРОМ 1£N */

SUM = 0.0; I = 1;

DO WHILE (I £ N);

/* SUM = X(L) + ... + X(I – L) AND 1 £ I £ N+1*/

SUM = SUM + X(I);

I = I + 1;

END;

/* SUM = X(L) + ...... + X(N) */

Предполагается, что приведенный фрагмент программы вычисляет
SUM = Х(1) +... + X(N). Вычисления организуются на основе цикла
DO WHILE. Эта конструкция означает, что повторяется нуль или более раз выполнение всех операторов, расположенных между оператором DO WHILE и соответству­ющим ему оператором END, до тех пор, пока условие в операторе DO WHILE истинно. Утверждение, записанное в форме примечания сразу же за оператором DO WHILE, следует считать связанным с точкой, непосредственно пред­шествующей проверке в этом операторе, т. е. считается, что оно должно быть справедливым каждый раз, когда мы попадаем в эту точку.

Доказательство частичной правильности для этой простой программы довольно очевидно. Для этого нужно просмотреть все пути в программе.

1. Путь от начала фрагмента программы до точки, непосред­ственно предшествующей проверке в операторе DO WHILE. Когда мы попадем в эту точку, будем иметь SUM = 0.0 и I=1. Утверждение, что SUM =Х(1)+...+ Х(I–1), очевидно спра­ведливо, так как I – 1 = 0, и мы считаем, что «пустая» сумма равна нулю. Утверждение 1 £ I < N + 1 также справедливо, ибо I = 0 и N ³ 1.

2. Путь от проверки в операторе DO WHILE через тело цикла вновь к проверке в операторе DO WHILE. Предположим, что до прохода по этому пути I = IN и справедливо указанное утверждение, т. е. IN £ N + L и SUM = X(L) + +... + X(IN – L). После того как мы пройдем по нашему пути, получим
SUM = [X(L) + ... + X(IN – L)] + X(IN) и I = IN + L. Следова­тельно, опять справедливо утверждение SUM = Х(1) + + Х(I – 1). Но мы проходим по этому пути лишь в случае истинности условия IN £ N. Таким образом, когда мы вернемся в точку проверки в операторе DO WHILE, будем снова иметь 1 £ IN + L = I £ N + 1.

3. Путь от проверки е операторе DO WHILE до точки, расположенной сразу же после конца цикла. По этому пути мы проходим, если условие в операторе DO WHILE ложно, т. е. I £ N дает ответ «ложь». Если при этом учесть, что иметь 1 £ I £ N + 1, то очевидно, что I = N + 1. Из этого факта, а также из справедливости утверждения SUM = X(1) + ...+ Х(I – 1) следует, что при достижении точки сразу же после цикла DO WHILE

SUM = X(L) + ... + X((N + 1) – 1) = X(L) + ... + X(N),

что и требовалось доказать.

Для доказательства конечности программы нужно только показать, что заканчивается сам цикл. Это, однако, очевидно, так как I увеличивается на 1 каждый раз при прохождении цикла, а значение N не изменяется. Следовательно, I в неко­торый момент станет больше N, и проверка I £ N даст отрицательный результат.

ПРИМЕР 2

/* M, N УЖЕ ИМЕЮТ ЦЕЛЫЕ ЗНАЧЕНИЯ И 0 £ N */

1 = 1; J=M; K=N;

DO WHILE (K ¹ 0);

/* (I*(J**K) = M**N AND 0 £ K */

DO WHILE (MOD (K, 2) = 0);

/* I*(J**К) = M**N AND 0 < K */

K = K/2E0;

J = J*J;

END;

K = K – 1;

I = I*J;

END;

/* I = M**N */

Мы хотим доказать, что приведенная программа на языке ПЛ/1 вычисляет I=M**N. Для доказательства частичной правильности нашего фрагмента рассмотрим следующие пути в программе:

1. Пусть от начала программы до точки, предшествующей непосредственно проверке во внешнем операторе DO WHILE. Когда мы попадем в эту точку, будем иметь I = 1, J = M и K = N. Таким образом, I*(J**K) = 1*(M**N)= = M**N, кроме того, 0 £ N = К. Следовательно, утверждение, связанное с точкой, предшествующей проверке во внешнем операторе DO WHILE, справедливо.

2. Путь от проверки во внешнем цикле до проверки во внутреннем цикле. На этом пути выясняется лишь, что К ¹ 0. Следовательно, связанное с внутренним оператором DO WHILE утверждение должно быть справедливым.

3. Путь от проверки во внутреннем операторе DO WHILE по внутреннему циклу с возвратом к проверке во внутреннем операторе DO WHILE. Предположим, что до прохода по этому пути I = IN, J = JN и К = КN. Кроме того, мы знаем, что IN*( JN**KN) = M**N и 0 < КN. Так как мы проходим по этому пути, то, следовательно, MOD (KN, 2) = 0, т. е. КN без остатка делится на 2. Пройдя по телу цикла, мы получим I = IN, К = КN /2Е0 и J = JN*JN. Следовательно, I*(J**K) = IN*[(JN* JN)**KN/2E0] = IN*(JN** KN/2E0)*(JN**KN/2E0) =

= IN* (JN** (KN/2E0 + KN/2E0) = IN* (JN** KN) = M**N

так как KN делится без остатка на 2. Кроме того, так как 0 < К и К делится без остатка на 2, должно выполняться отношение K = KN /2E0 > 0. Таким образом, утверждение, относящееся к внутреннему оператору DO WHILE, в момент возврата к нему должно быть справедливо.

4. Путь от проверки во внутреннем операторе DO WHILE к окончанию внешнего цикла и возврат к проверке во внешнем операторе DO WHILE. Предположим, что мы находимся во внутреннем операторе DO WHILE,
I = IN, J = JN и К = КN. В этот момент справедливы утверждения IN*(JN**KN) = = M**N и 0 < КN. Кроме того, если мы проходим по указанному пути, проверка во внутреннем DO WHILE дает отрицательный ответ, т. е. условие MOD(KN, 2) = 0 ложно. Пройдем до конца внешний цикл и вернемся к проверке во внешнем операторе DO WHILE. Теперь будем иметь К = KN – 1,
I = IN* JN и J = JN. Следовательно, в этот момент

I*(J**K) = (IN* JN)*[JN** (KN – L)] = IN*[JN*( JN **(KN – L))] =

= IN*[JN**(1 + KN – 1)] = IN*(JN** KN) = M**N.

Кроме того, так как 0 < КN, то 0 < КN – 1 = К. Таким образом, связанное с внешним оператором DO WHILE утверждение снова оказывается справедливым.

5. Путь от проверки во внешнем операторе DO WHILE do точки, расположенной непосредственно после конца внешнего цикла. Если мы прошли этим путем, условие К ¹ 0 было ложным, т. е. К = 0. Утверждение, соответствующее внешнему циклу, справедливо, т. е. I*(J**K) = M**N. Однако, поскольку мы вышли из цикла,

I*(J**K) =I*(J**0) = I*(1) = I = M**N,

что и требовалось доказать.

Для доказательства выполнения данной программы нужно показать, что если мы попадем во внешний или внутренний цикл, то эти циклы обязательно закончатся. Сначала рассмот­рим внутренний цикл. Отметим, что при каждом прохождении цикла значение К устанавливается равным К/2Е0, т. е. К все время уменьшается. Следовательно, в какой-то момент его значение уменьшится настолько, что не будет без остатка делиться на 2 В этот момент условие MOD(K, 2) = 0 станет ложным, что и гарантирует окончание внутреннего цикла. Теперь рассмотрим внешний цикл. Отметим, что при каждом прохождении по внешнему циклу значение К уменьшается по крайней мере на 1. Действительно, если при этом мы проходим несколько раз внутренний цикл, то К уменьшается на соответствующую степень 2. Если внутренний цикл не выполнялся, то перед выходом из внешнего цикла значение

К стало равным К – L Таким образом, в любом случае значе­ние К уменьшилось по крайней мере на 1. Так как известно, что 0 £ К, то значение К в конце концов станет равным 0. В этот момент условие К = 0 будет истинным, и внешний цикл закончится.

3.4. Доказательство частичной правильности как
часть процесса программирования

Все примеры доказательства правильности в этом учебном пособии относились к законченным и небольшим программам. Однако на практике такое доказательство должно проводиться программистом во время самого процесса программирования. Не следует ожидать, что кто-нибудь возьмет большую, закон­ченную программу и начнет доказывать ее правильность. Интеллектуальные затраты на такую работу были бы, вероятно, очень велики. Нужно доказывать правильность небольших фрагментов по мере того, как они составляются. Для того чтобы это можно было делать, такие секции (фрагменты) не должны вместе образовывать запутанный клубок, где не найдешь ни конца, ни начала каждой. Многие утверждают, что программист сможет избежать излишних необходимых усложнений и запутанных структур, если он не будет использовать переходы GO TO и ограничит себя небольшим множеством операторов управления с одним входом и одним выходом. Такими операторами могут быть: последовательное выполнение, условное выполнение (ветвление) вида IF С THEN SI ELSE S2 и итеративная конструкция основного вида WHILE С DO S. Программы, написанные в таком стиле, часто называют «структурирован­ными» программами. Тем не менее использование такого ограниченного подмножества операторов управления, конечно, не спасает программиста от всех «болезней». И с такими операторами управления, как и с оператором GO TO, можно написать «мрачную» программу, которую трудно понять и верифицировать. Важно, чтобы программа была ясна по замыслу и при этом не использовались такие операторы управления, которые запутывают связи между отдельными частями (путем переходов вперед или назад с использованием оператора GO TO).

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

Выполнение таких операторов будет приводить к справедли­вости некоторых постусловий (утверждений о правильности такой подчасти) при условии, что до выполнения были справедливы предусловия (входные утверждения для этой подчасти). Таким образом, доказывая правильность большого фрагмента, вовсе нет необходимости разбираться во всех его частях. Часто процесс идет в обратном порядке, т. е. про­граммист, работая по принципу «сверху вниз», составляет большой фрагмент, оставляя неопределенным в данный момент некоторые его части. Доказывая правильность этого фрагмента, он исходит из того, что упомянутые части будут написаны так, что их выполнение будет приводить к справед­ливости некоторых постусловий, если до их выполнения были справедливы предусловия. После этого, опираясь на эти утверждения, доказывается правильность большого фраг­мента. Позже, при составлении программ для более мелких частей, для доказательства их правильности нужно лишь показать, что из допущения справедливоети до их выполнения предусловий следует справедливость после выполнения постусловий.

Как уже говорилось в п. 2.5, мы не считаем, что программисту необходимо выписывать все пункты дока­зательства правильности. Однако он должен выписывать все ключевые утверждения (как примечания), а затем удосто­веряться в их справедливости (без деталей). Программист должен (без лишних подробностей) удостовериться и в том, что программа в конце концов закончит работу.

Основная мысль этого раздела заключается в том, что не­формальное доказательство правильности следует проводить в процессе программирования, а не после того, как программа написана.

Литература

Доказательство правильности программ / М.: Мир, 1982.