Доказательство корректности строк 14-18 выглядит точно так же, поэтому теперь мы можем считать, что мы доказали правильность всех трех ветвей оператора case. Одна из ветвей корректно завершает цикл, а другие две сохраняют истинность инварианта.
Этот анализ показывает, что если цикл завершается, то значение р оказывается истинным. Однако мы все еще можем попасть в ситуацию с бесконечным циклом.
На самом деле именно таким был результат ошибок, допущенных большинством профессиональных программистов.
Доказательство конечности использует другой аспект диапазона L.u. Этот диапазон изначально имеет некоторый конечный размер (п), и строки с 6-й по 9-ю гарантируют, что цикл будет завершен, когда в диапазоне окажется менее одного элемента. Следовательно, нужно показать, что диапазон уменьшается при каждой итерации. Строка 12 говорит, что m всегда принадлежит текущему диапазону. Обе ветви оператора case, в которых выполнение цикла не прерывается (строки 14 и 22), исключают значение m из текущего диапазона и, следовательно, уменьшают его но меньшей мере на 1 элемент. Таким образом, программа обязательно должна завершиться.
Теперь я практически уверен, что мы можем пойти дальше и закодировать функцию па С. В следующей главе мы займемся именно этим — реализацией функции на языке С и проверкой ее корректности и эффективности.
Опубликовал vovan666
April 16 2013 23:58:07 ·
0 Комментариев ·
3634 Прочтений ·
• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •
Комментарии
Нет комментариев.
Добавить комментарий
Рейтинги
Рейтинг доступен только для пользователей.
Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.
Нет данных для оценки.
Гость
Вы не зарегистрированны? Нажмите здесь для регистрации.
Главная
Каталог файлов
