Ветка подходящая... Давайте зафиксируем для новичков два базовых паттерна циклов.

Итак, полный проход - есть некая последовательность... чего угодно. Элементов, шагов, ситуаций... Длина не известна, но известно условие проверки её окончания. Т.е. имеет место вот эта самая "обратная связь" - продвинулись на шаг, проверили, не достигнута ли ещё цель.

Схема "полный проход"

## Код:
```
взять_первую_ситуацию;
WHILE ~конец_ситуаций (* т.е. "удалось взять очередную ситуацию" *) DO
  (* Предусловие: имеем текущую ситуацию, подлежащую обработке *)
  полезное_действие_в_текущей_ситуации;
  переход_к_следующей_ситуации
END
```


Если видим полный проход в задаче, то сводим его строго к такому шаблону, без фантазий.

Пример с потоковым чтением. Правильно организованный интерфейс потокового чтения предоставляет функцию "считать очередной элемент" и признак, который показывает, было ли считывание успешным.
## Код:
```
reader.Read(elem);
WHILE reader.Done() DO
  ...работаем с elem...
  reader.Read(elem)
END
```

Очевидно, что попыток чтения и должно быть на одну больше, чем оборотов цикла с полезным действием. И "дублирование" как раз по этой причине возникает, и любые попытки его "убрать" не приведут к прояснению ситуации, а только к запутыванию и потере прозрачности.

В других случаях начальное действие и переход могут быть разными:
## Код:
```
it := items;
WHILE it # NIL DO
  ...работаем с it...
  it := it.next
END
```


Действия "взять_начальную", "перейти_к_следующей", не говоря про само полезное действие, могут быть сколь угодно необычными, самое главное - узнать саму семантику полного прохода, и без фантазий написать по шаблону.

Схема "линейный поиск"

Та же история - последовательность чего угодно... Задача - найти такую ситуацию, которая удовлетворяет условию поиска, или показать, что её нет (достигли конца последовательности).

## Код:
```
взять_первую_ситуацию;
WHILE ~конец_ситуаций & ~( ... условие поиска ..) DO
  ... возможно, но не очень часто встречается  - действие над текущей ситуацией ...
  взять_следующую_ситуацию
END;
IF ~конец_ситуаций THEN
  ... нашли, делаем что надо, с той ситуацией, на которой остановился цикл...
ELSE
  ... не нашли, делаем что-то, если нужно
END
```


Важно, чтобы & вычислялся сокращённо (в нормальных языках так и есть), т.к. условие поиска может не иметь смысл в случае конец_ситуаций.

Касательно Дракона - там не нужно повторять IF после цикла, там за счёт разделения конъюнкции WHILE на две последовательных проверки получается два параллельных исхода из цикла - "нашли" и "не нашли", на которые и нанизываем дальнейшие действия. Очень выразительно.
viewtopic.php?p=21377#p21377

Касательно этого был ещё тут пример -viewtopic.php?f=7&t=1443
Про то, что как только узнали стандартную схему, дальше лучше "без фантазий".

Пример с "узнаванием" линейного поиска  (Из программки одного моего студента)

Имеется граф потока вычислений. Т.е. ориентированный граф без циклов, вершина - это операция, по дугам входят аргументы. Его можно обсчитывать в режиме потока данных (распространяя "волну" от аргументов к результатам), а можно "лениво" (от интересующего нас конечного узла запрашивая рекурсивно назад).
Если считаем в первом режиме, то возникает "фронт волны" (или ещё говорят "рабочая стопка", workpile).
Так вот, на каждом витке workpile-алгоритма мы ищем в стопке те узлы графа, для которых уже готовы все аргументы.

Нужно написать для узла графа функцию ReadyForCalc(node): BOOLEAN.
Понимающий студент сразу видит, что это = "для любого непосредственного предка node выполнено defined".
Т.е.A anc : anc IN Ancestors(node) : anc.defined, где A - квантор всеобщности, A. Точно так же он знает, что это эквивалентно~ ( E anc : anc IN Ancestors(node) : ~anc.defined, т.е. "среди предков не существует такого, для которого ~defined". Т.е. чтобы доказать, что "для любого..." нужно построить "опровергающий" линейный поиск обратного условия и вернуть отрицание результата этого поиска.
Ну и конкретно это отображается в код (граф хранится на квадратной матрице, так, как его вводят в редакторе - для простоты, чтоб не грузить студента ещё задачей авторазмещения элементов на листе):

## Код:
```
PROCEDURE ReadyForCalc (g: Flow.Grid; ref: Flow.Ref): BOOLEAN;
      VAR j: INTEGER; cell: Flow.Cell;
   BEGIN
      (* A cell : cell IN Anc(g[ref]) : cell.defined *)
      (* ~ ( E cell : cell IN Anc(g[ref]) : ~cell.defined *)
      (* т.е. линейный поиск ячейки с ~cell.defined. RETURN поиск_не_удался *)
      ASSERT (g[ref.x, ref.y].argCount > 0, 20);
      cell := g[ref.x, ref.y];
      j:= 0;
      WHILE (j < cell.argCount) & g[cell.args[j].x, cell.args[j].y].defined DO
         INC(j);    
      END;
      RETURN j = cell.argCount
   END ReadyForCalc;
```


Вот эта вот задача - проверка выполнения какого-то условия для всех ситуаций - тоже часто встречается, её надо узнавать и по такой схеме трансформировать в "опровергающий" линейный поиск.

Наконец, и сам цикл продвижения волны по графу тоже сводится к шаблонному полному проходу, надо только понять, какая тут последовательность ситуаций. За ситуацию примем набор необсчитанных пока вершин, хранящихся в рабочей стопке (фронте).
Т.е. инвариантом цикла будет (* INV: в front находятся ещё не обсчитанные вершины, ~defined *).
При этом очевидно, что целесообразно хранить в стопке непосредственно только те вершины, которые имеют шанс стать обсчитанными на очередном витке.

Заведём две операции: Calc ищет в стопке те узлы, которые ReadyForCalc и выполняет расчёт их значений.
Step ищет в стопке обсчитанные вершины (они там могут оказаться в середине витка цикла, когда инвариант временно нарушен после Calc), выбрасывает их из стопки, а взамен помещает их непосредственных последователей (тех, которые ещё не попали).
Имеем полный проход:
## Код:
```
поместить_в_стопку_начальные_аргументы;
Step;
WHILE количество_в_стопке > 0 DO
  Calc;
  Step
END
```


Как всегда, с помощью первой части тела цикла мы продвинулись вперёд, но нарушили соотношение-инвариант, с помощью второй - восстановили инвариант, после чего идёт проверка условия окончания.

Всего-то и делов.

Поподробнее об инварианте цикла.
Инвариант - "рельсы", по которым он едет - что истинно до начала цикла ("поставили на рельсы") и в конце каждого витка. (А раз в конце каждого витка, то и после завершения цикла тоже. Вот ещё одна причина не делать досрочных выходов из цикла. Тогда пишущему и читающему придётся дополнительно убеждаться, что в каждом месте цикла, где он прерывается, инвариант восстановлен.)

Вот тут ещё было об инварианте:
viewtopic.php?p=21375#p21375

Ну что, неужто такая "жуткая математика"? Простые, естественные рассуждения, ровно настолько формальные, насколько это удобно, чтобы "иметь почву под ногами".