строки 25 при условии, что утверждение строки 24 верно, сохраняет истинность строки 26 - это определение операции присваивания. Таким образом, эта ветвь оператора case переопределяет инвариант в строке 27.
Доказательство для строк 14-02 имеет в точности такой же вид, как и доказательство для всех трех переходов по оператору case. Один из них корректно завершает цикл, а два других сохраняют инвариант.
Анализ программы показывает, что при завершении цикла переменная Р имеет правильное значение. Однако цикл может оказаться бесконечным; действительно, это было наиболее распространенной ошибкой в программах, написанных профессиональными программистами.
В доказательстве конечности алгоритма используется другая часть области L . . . U. Первоначально эта область состоит из некоторого конечного числа элементов (N), а строки 6-9 гарантируют, что цикл завершится, когда в области будет меньше одного элемента. Поэтому, чтобы доказать конечность алгоритма, нужно показать, что область сокращается при каждом проходе по циклу. В строке 12 нам сообщается, что индекс М всегда находится в текущей области. Оба зацикленных ветвления в операторе case (строки 14 и 22) исключают элемент, имеющий индекс М, из текущей области, и поэтому уменьшают ее размер по крайней мере на 1, следовательно, программа должна завершиться.
4.4. РЕАЛИЗАЦИЯ ПРОГРАММЫ
До сих пор мы работали с программой на псевдоязыке высокого уровня. Наше желание использовать подходящие структуры управляющей логики позволяло нам игнорировать особенности какого-либо конкретного языка программирования и сосредоточить внимание на сути проблемы. Однако в конечном счете нам придется писать программу на реально существующем языке. Именно для того, чтобы вы не думали, что я выбрал язык, облегчающий задачу, двоичный поиск был реализован на Бейсике. Хотя некоторые задачи решать с помощью программ, написанных на Бейсике, и хорошо, бедность его управляющих структур, а также глобальные (и обычно короткие) имена переменных являются существенным препятствием для создания реальных программ.
Но даже несмотря на эти проблемы приведенный выше псевдокод может быть легко выражен на диалекте языка Бейсик. В строках 1010 - 1045 содержится краткая спецификация подпрограммы.
1000 '
1010 * ДВОИЧНЬЙ ПОИСК Т В МАССИВЕ Х(1..М)
1020 » ВХОД: Х(1..Н) - ОТСОРТИРОВАН В НЕУБЫВАЮЩЕМ ПОРЯДКЕ
57
