Ветвление осуществляется операторами if и case в различных формах. При выполнении программы выбирается одна из возможных ветвей. Корректность доказывается путем индивидуального разбора каждой из ветвей. Факт выбора данной ветви дает возможность сделать некоторые утверждения в нашем доказательстве; если мы выполняем оператор, следующий за if i>j, то мы можем сделать утверждение, что i>j, и использовать это для вывода следующего подходящего утверждения.
Циклы
Для доказательства корректности цикла нужно рассмотреть три его части: инициализацию, сохранение (инварианта) и завершение (рис. 4.1).
Рис. 4.1. Три составные части цикла
Сначала мы доказываем, что инвариант цикла устанавливается при инициализации, а затем показываем, что на всех итерациях его истинность сохраняется. Эти два этапа гарантируют (по методу математической индукции), что инвариант остается истинным перед и после каждой итерации цикла. Третий этап: доказательство того, что при любом варианте завершения цикла результат оказывается корректным. Все это вместе гарантирует, что если цикл завершится, то результат будет правильным. Сходимость доказывается отдельно (типичный пример — доказательство сходимости двоичного поиска, приведенное выше).
Опубликовал vovan666
April 16 2013 23:58:11 ·
0 Комментариев ·
2867 Прочтений ·
• Не нашли ответ на свой вопрос? Тогда задайте вопрос в комментариях или на форуме! •
Комментарии
Нет комментариев.
Добавить комментарий
Рейтинги
Рейтинг доступен только для пользователей.
Пожалуйста, залогиньтесь или зарегистрируйтесь для голосования.
Нет данных для оценки.
Гость
Вы не зарегистрированны? Нажмите здесь для регистрации.
Главная
Каталог файлов
