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

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

Таким образом, для простых программ с одним циклом основными приемами при доказательстве правильности блок-схем являются:

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

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

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

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

Для того, чтобы яснее представлять этапы доказательства правильности, будем «приписывать» ключевые утверждения, которые необходимо доказать, непосредственно тем точкам блок-схемы, к которым они относятся (рис. 2.2).

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

Рис. 2.1 Рис. 2.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 в этой точке принимают значения I_n и J_n, т.е. J_n = I_n∙ N. Если I ¹ M ложно, то это уже обеспечивает конечный результат. Предположим теперь, что мы прошли по циклу (от точки 2 через точки 3, 4 вновь в точку 2), что возможно только при выполнении условия I ¹ M. При возвращении в точку 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.

Теперь докажем, что в конце концов попадем в точку 2 со значением I = M. При первом попадании в точку 2 имеем I =0. При последующих попаданиях, если таковые есть, I каждый раз увеличивается на 1. Так как значение M нигде в программе не изменяется и мы предположили, что M ³0, то очевидно, что в какой-то момент I станет равным M.

Если мы попадем в точку 2 при I = M, то будет верно и J = I ∙ N = M ∙ N. Отношение I ¹ M в этот момент ложно, и мы попадаем по стрелке с пометкой F (FALSE – ложь) в точку 5 с J = M ∙ N. На этом доказательство правильности программы заканчивается.

Дополнительные примеры доказательства правильности блок-схем простых программ (с одним циклом) можно посмотреть в [1].

Упражнения

1. Докажите, что программа (рис. 2.3) вычисляет произведение M на N при условии, что M и N имеют целые значения и M ³ 0. Что произойдет, если M < 0?

2. Предположим, что на блок-схеме (рис. 2.3) по ошибке вместо проверки i = 0 стоит проверка i = 1. На каких этапах доказательства правильности это выяснится? Предположим, что J по ошибке получает начальное значение 1, а не 0. Где это выяснится при доказательстве? Представим себе, что J присвоено вначале значение N, а не 0 и, кроме того, проверка идет на i = 1. Для каких значений данных программа будет верно вычислять произведение M ∙ N? Как это показать, исходя из доказательства правильности?

3. Докажите, что программа (рис. 2.4) вычисляет и печатает значение M ^N. Предполагается, что M и N – целые числа, причем и1 £ M и 1 £ N. Будет ли эта программа работать правильно, если в качестве N введено значение 0? Измените блок-схему так, чтобы программа работала правильно и при N = 0.

Рис. 2.3 Рис. 2.4

4. Докажите, что программа (рис. 2.5) вычисляет и печатает значение
M! = 1 × 2 × 3 ×... × (M – 1) × M при условии, что в качестве M вводится положительное целое число.

5. Докажите, что если в программу (рис. 2.6) в качестве значений I и J вводятся соответственно I ₀ и J ₀, причем 0 £ I ₀, то печатаемые в конце значения
I и J будут соответственно 0 и J ₀ + 2 × I ₀.

Рис. 2.5 Рис. 2.6

6. Для программ, блок-схемы которых приведены на рис. 2.7–2.8, определите, при каких значениях данных программа будет заканчиваться. Найдите эти значения также для случаев, когда:

а) на рис. 2.7 проверка I £ M заменена на I £ M;

б) на рис. 2.8 команда I ← I + 1 заменена на I ← I + 2;

Рис. 2.7 Рис. 2.8

Конфликты в семейной жизни. Как это изменить? Редкий брак и взаимоотношения существуют без конфликтов и напряженности. Через это проходят все...

Что делает отдел по эксплуатации и сопровождению ИС? Отвечает за сохранность данных (расписания копирования, копирование и пр.)...

Что будет с Землей, если ось ее сместится на 6666 км? Что будет с Землей? - задался я вопросом...

Что делать, если нет взаимности? А теперь спустимся с небес на землю. Приземлились? Продолжаем разговор...

Не нашли то, что искали? Воспользуйтесь поиском гугл на сайте: