ВУЗ:
Рис. 4.21. Решение задачи с помощью лишь одного разреза
Третье утро. Отдать владельцу отеля одно звено.
Четвертое утро. Забрать у владельца отеля три отданные ему ранее звена и отдать ему фрагмент цепочки из четырех
звеньев.
Пятое утро. Отдать владельцу отеля одно звено.
Шестое утро. Забрать у владельца отеля одно звено и отдать ему фрагмент цепочки из двух звеньев.
Седьмое утро. Отдать владельцу отеля одно звено.
Следовательно, тот ответ, который мы считали правильным, на самом деле неверен. Как же убедиться, что новое реше-
ние действительно правильно? В качестве доказательства можно привести следующее рассуждение. Поскольку в первое ут-
ро необходимо отдать владельцу отеля одно звено, придется разрезать, по крайней мере, одно звено цепочки. Но так как в
новом варианте решения требуется разрезать только одно звено, то это решение должно быть оптимальным.
Применительно к программированию этот пример демонстрирует различия между программой, которая выглядит пра-
вильной, и программой, которая действительно является правильной. Это не всегда одно и то же. Специалистам в области
обработки данных известно множество ужасных историй о том, как программное обеспечение, которое считалось безуслов-
но правильным, все же отказывало в критический момент, поскольку возникшая ситуация оказывалась для него совершенно
непредвиденной. Следовательно, верификация программного обеспечения – это важное и необходимое дело, а поиск эффек-
тивных методов верификации является активным направлением исследований в области компьютерных наук.
Одно из самых современных направлений в этой области заключается в использовании методов формальной логики для
доказательства корректности программ. Это означает, что цель проводимых исследований состоит в применении формаль-
ной логики для доказательства того факта, что реализованный данной программой алгоритм делает именно то, для чего он
предназначен. Основополагающий тезис заключается в том, что при сведении процесса верификации к формальной проце-
дуре мы застрахованы от некорректных умозаключений, вытекающих из интуитивной аргументации, как это было в случае с
задачей о золотой цепочке. Давайте рассмотрим данный подход к верификации программ более подробно.
Подобно тому, как формальное математическое доказательство основывается на аксиомах (геометрические доказатель-
ства часто базируются на аксиомах Евклидовой геометрии, тогда как доказательства других утверждений – на аксиомах тео-
рии множеств), формальное доказательство правильности программы основывается на спецификациях, в соответствии с ко-
торыми эта программа разрабатывалась. Чтобы доказать, что программа правильно сортирует списки имен, мы можем на-
чать с предположения о том, что на вход программы подается список имен. Если программа создана для вычисления средне-
го значения одного или более положительных чисел, мы можем предположить, что исходными данными для программы яв-
ляется одно или несколько положительных чисел. Короче говоря, доказательство корректности начинается с предположения
о том, что в начале работы программы удовлетворены некоторые условия, называемые предварительными условиями (pre-
condition), или предусловиями.
Следующий этап доказательства корректности заключается в рассмотрении того, как следствия из этих предусловий
распространяются по программе. С этой целью исследователи изучили различные программные структуры, пытаясь устано-
вить, как выполнение данной структуры влияет на утверждение, о котором до выполнения этой структуры было известно,
что оно истинно. Например, пусть определенное утверждение о значении переменной Y перед выполнением приведенной
ниже инструкции было истинно:
X ← Y
После выполнения этой инструкции то же утверждение можно сделать о значении переменной X. Например, если перед
выполнением инструкции значение переменной Y отличалось от 0, то можно сделать заключение, что после выполнения
этой инструкции значение переменной X также будет отличаться от 0.
Несколько более сложным случаем является выполнение оператора if-then-else, например, следующего вида:
if (условие) then {инструкция 1} else {инструкция 2}.
Если в этом примере известно, что некоторое утверждение было истинно перед выполнением данной структуры, то не-
посредственно перед выполнением инструкции 1 мы знаем, что истинны как это утверждение, так и проверяемое условие. В
то же время, если должна выполняться инструкция 2, мы знаем, что должны быть истинны исходное утверждение и отрица-
ние проверяемого условия.
Верификация требуется не только программному обеспечению. Обсуждаемые в тексте проблемы верификации касаются не толь-
ко программного обеспечения. Столь же важно получить гарантии, что выполняющая программу аппаратура также не содержит ошибок.
Это подразумевает верификацию как разрабатываемых схем, так и конструкции всей машины. И в этом случае полученные результаты в
значительной степени зависят от тестирования, задача которого, как и в случае с программным обеспечением, – выявить скрытые ошибки.
Показателен пример машины Mark 1, созданной в Гарвардском университете в 1940 г., монтажные ошибки в которой оставались необна-
руженными в течение многих лет. Более "свежий" пример – ошибки в блоке выполнения операций с плавающей точкой, имевшие место в
первых микропроцессорах типа Pentium. В обоих случаях существующие ошибки были выявлены до каких-либо серьезных последствий.
Страницы
- « первая
- ‹ предыдущая
- …
- 99
- 100
- 101
- 102
- 103
- …
- следующая ›
- последняя »
