Я давно собирался написать статью по этому вопросу, да как-то все руки не доходят. Но, поскольку здесьviewtopic.php?f=27&t=3157&start=40в очередной раз разгорелся базар по этому поводу, то напишу кое-какие тезисы.

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

Что касается инварианта цикла, которой традиционно проверяется "перед циклом", то уже становится ясно, что в данном случае инвариант нужно проверятьвнутрицикла, в точке перед условием выхода.

Вот и все.
Все наработки для цикловwhileостаются в силе (в том числе и весь бред про линейный поиск, для любителей).

В заключение надо отметить, что с эстетической точки зрения цикл с выходом из середины выглядит, конечно, отвратно. И вреден для неокрепших умов. Здесь - самое главное иметь четкую картину в голове. И укреплять ум(ы).