Урок 35
Доказательство правильности программ
(§37. Доказательство правильности программ)

Содержание урока

Как доказать правильность программы?

Алгоритм Евклида

Инвариант цикла

Спецификация

Вопросы и задания

Задачи

Вопросы и задания

1. Зачем нужно доказывать правильность программ?
2. Расскажите о двух подходах к проверке правильности программ.
3. Почему с помощью тестирования сложно доказать правильность программы? В каких случаях это всё же можно сделать? Приведите примеры.
4. Что изменится в доказательстве алгоритма Евклида, если тип — это произвольные натуральные числа (неравенство m ≥ n может не выполняться)?
5. Что такое инвариант цикла?
6. Зачем нужно определять инвариант цикла?
7. Что такое спецификация? Почему желательно формулировать её в виде формальных утверждений, а не на естественном языке?
8. Объясните запись {Q}S{R}.
9. Какая программа называется корректной?
10. Как вы думаете, можно ли назвать корректной программу, которая «зависает» при неверных входных данных? Обсудите этот вопрос в классе.
11. Что такое верификация программы?
12. Как вы думаете, что сложнее — доказывать правильность готовой программы или сразу писать программу, доказывая правильность отдельных блоков? Почему? Обсудите этот вопрос в классе.

Следующая страница Задачи

Cкачать материалы урока