Я давно собирался написать статью по этому вопросу, да как-то все руки не доходят. Но, поскольку здесь viewtopic.php?f=27&t=3157&start=40 в очередной раз разгорелся базар по этому поводу, то напишу кое-какие тезисы.
Итак, имеем обобщенный цикл вида
Код:
цикл
последовательность команд Х
что-нибудь типа exit или break по условию
последовательность команд Y
конец цикла
Середину с выходом можно гонять как слайдер вверх-вниз и получать граничные случаи: цикл while и цикл repeat..until. Это хорошо.последовательность команд Х
что-нибудь типа exit или break по условию
последовательность команд Y
конец цикла
Плохо то, что формальный аппарат, описанный у Дейкстры-Грисса можно применять вроде бы только для циклов типа while.
В принципе, Кнут приводит аксиоматизацию Дала для обобщенного цикла:
Цитата:
Пусть: {P}S{Q} {Q & B}T{P}
Тогда: {P} loop: S; while B : T; repeat; {Q & ~B } (стр. 49)
В ней нет ничего сложного, но для простого программиста польза от этой записи равна строго нулю. Тогда: {P} loop: S; while B : T; repeat; {Q & ~B } (стр. 49)
Тем не менее, все не так плохо. Надо только ответить на 2 вопроса.
1. Что является телом обобщенного цикла?
2. В какой точке цикла нужно проверять инвариант цикла?
Ответить на эти вопросы проще, чем их поставить.
Если немного подумать, то легко понять, что телом цикла является кусок Y;X. Т.е., чтобы рассуждать о таком цикле, нужно просто мысленно подставить вехний кусок X под нижний Y. А вся конструкция эквивалентна последовательности
Код:
X;
пока условие цикл
Y;
X;
конец цикла
Здесь как раз и вылезает то самое дублирование кода.пока условие цикл
Y;
X;
конец цикла
Что касается инварианта цикла, которой традиционно проверяется "перед циклом", то уже становится ясно, что в данном случае инвариант нужно проверять внутри цикла, в точке перед условием выхода.
Вот и все.
Все наработки для циклов while остаются в силе (в том числе и весь бред про линейный поиск, для любителей).
В заключение надо отметить, что с эстетической точки зрения цикл с выходом из середины выглядит, конечно, отвратно. И вреден для неокрепших умов. Здесь - самое главное иметь четкую картину в голове. И укреплять ум(ы)
.
