Постусловием цикла (P) называется отрицание его условия (C), то есть P = не C. Инвариантом цикла (I) — утверждение, верное до и после любого выполнения цикла. Нас интересуют I такие, что утверждение I и не P является тем, что мы хотим доказать. Таким образом, для доказательства правильности работы программы необходимо сформулировать, что делает каждый ее цикл, доказать, что он нормально завершается, при необходимости предъявить соответствующий инвариант и доказать его индукцией по проходам цикла.
1.
Дано: Робот в огороженном прямоугольнике.
Надо: Робот у северной стены.
2.
Дано: Робот в огороженном прямоугольнике.
Надо: Робот в северо-западном углу.
3.
Дано: Робот в нижней (южной) клетке огороженного коридора шириной в одну клетку.
Надо: Все клетки коридора закрашены.
Примечание: Желательно найти два решения с различными инвариантами.
4.
Дано: Робот в юго-западном углу прямоугольника.
Надо: Прямоугольник закрашен.
5.
Дано: Робот в нижней клетке незакрашенного коридора шириной в одну клетку..
Надо: Клетки закрашены через одну, начиная с первой.
6.
Дано: Робот в нижней клетке незакрашенного коридора шириной в одну клетку..
Надо: Клетки закрашены через одну, начиная с первой..
3. Дано: Робот в нижней (южной) клетке огороженного коридора шириной в
Надо: все клетки коридора закрашены.
Примечание: желательно найти два решения с различными инвариантами.
4. Дано: Робот в юго-западном углу прямоугольника.
Надо: прямоугольник закрашен.
5. Дано: Робот в нижней клетке незакрашенного коридора шириной в одну клетку.
Надо: Клетки закрашены через одну, начиная с первой.
6. Дано: Робот в левом нижнем углу огороженного незакрашенного прямоугольника.
Надо: прямоугольник закрашен в шахматном порядке, левая нижняя клетка
Примечание. Высота или ширина прямоугольника (или обе) могут быть равны 1.
7. Дано: Робот у южной стены огороженного прямоугольника, внутри которого
только горизонтальные стены, все находящиеся на одной широте.
Надо: Робот у северной стены.
8. Дано: в огороженном прямоугольнике только горизонтальные стены, не
Надо: Робот у северной границы.
9. Дано: в огороженном прямоугольнике есть вертикальные и горизонтальные
стены, не примыкающие к границе прямоугольника и друг к другу.
Надо: Робот в северо-западном углу прямоугольника.
10. Дано: в огороженном прямоугольнике есть вертикальные и
горизонтальные стены, не примыкающие друг к другу (но, возможно,
примыкающие к границе) и не нарушающие связности.
Надо: Робот в северо-западном углу
11. Дано: в огороженном прямоугольнике есть не примыкающая к границе
огороженная со всех сторон клетка; других стен нет, Робот в
юго-западном углу.
Надо: Робот в клетке, соседней с огороженной.