Название: Доказательство правильности программ - Конспект лекций (Веретельникова Е.Л.)

Жанр: Экономика

Просмотров: 1604


      правильности блок-схем программ

 

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

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

Пример 2.4. Мы хотим доказать, что приведенная на рис. 2.4 блок-схема вычисляет и печатает среднее значение и максимальное из всех чисел во входном файле. Заметим, что в этом случае выход из цикла предполагается при выполнении условия цикла, что подразумевает использование цикла типа UNTIL, а не WHILE.

Сначала докажем, что справедливо утверждение, связанное с точкой 2.

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

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.4

 

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

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

Пример 2.5. Мы хотим доказать, что приведенная на рис. 2.5 блок-схема обеспечивает правильное вычисление суммы . Сначала покажем, что при каждом попадании в точку 2 выполняются соотношения 1£ I £ N + 1, и для 1< I £ N + 1 (Особый случай при I = 1: сумма 0 членов есть 0).

Рис. 2.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 и SUMn =

= . Если мы пройдем по циклу и вернемся в точку 2 (в случае истинности In £ N), то получим In+1 = In + 1 и

SUMn +1 = SUMn +  

= .

Кроме того, если цикл повторялся, то проверка In £ N давала положительный ответ, а так как истинно и утверждение 1 £ In £

£ N + 1, то, следовательно, 1 £ In £ N. Но в этом случае при возврате в точку 2 имеем 1< (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 =

= .

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

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

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

Рис. 2.6

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

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

K = LI оказалась истинной, т.е. LI = LJ = K. Однако мы также знаем, что ни один из элементов L1, ..., LI-1 = J-1 не был равен K (так как это справедливо в точке 2 и на пути от точки 2 до точки 7 значение I нигде не изменялось). Из этого следует, что в конце концов мы попадем в точку 7, и будет справедливо приведенное утверждение о правильности.