Самое смешное -- это то, что в Обероне нет цикла Дейкстры. Есть цикл, синтаксически напоминающий цикл Дейкстры, но семантически всё-таки отличающийся от него...
Впрочем, настоящего ветвления Дейкстры в Оберонах/Модулах-2 тоже нет, есть ветвление, лишь синтаксически напоминающее его.
Предлагаю раскрыть мысль, дабы народ сейчас не нафантазировал чего-то странного.
Ну сколько ж можно раскрывать эту простую мысль? Я об этом много раз повторял (больше трёх точно).
Вспоминаем, что Дейкстра писал в своей "Дисциплине программироания" про оператор if (и аналогичные рассуждения по поводу оператора do):
if B1 → SL1 □ B2 → SL2 □ ... □ Bn → SLn fi
do B1 → SL1 □ B2 → SL2 □ ... □ Bn → SLn do
где B1...Bn -- "предохранители", логические выражения охраняемых команд,
SL1...SLn -- списки операторов,
а B1 → SL1 -- охраняемая команда
1. Предполагается, что все предохранители определены; если это не так, т.е. вычисление какого-то предохранителя может привести к работе без правильного завершения, то допускается, что и вся конструкция не сможет правильно завершить свою работу.
2. Вообще говоря, наша конструкция приведёт к недетерменированности при тех начальных состояниях, для которых истинны значения более чем одного предохранителя, поскольку остаётся неопределённым, какой из соответствующих списков операторов будет тогда выбираться для запуска. Никакой недетерменированности не возникает, если все предохранители попарно исключают друг друга.
3. Если начальное состояние таково, что ни один из предохранителей не является истиной, то мы встречаемся с начальным состоянием, для которого не подходит ни один из вариантов, а следовательно, и вся конструкция в целом. Запуск при таком начальном состоянии приведёт к отказу.
Замечание. Если мы допускаем также и пустой набор охраняемых команд, то операторы "if-fi" и "do-od" семантически эквивалентны нашему прежнему оператору "Отказать".
Таким образом, для того, что бы операторы IF и WHILE в Обероне могли считаться операторами if и do Дейкстры (назовём их "Ветвлением Дейкстры" и "Циклом Дейкстры"), их предохранители быть написаны в предположении недетерменированного порядка вычисления, и если ни один из предохранителей не срабатывает, должен происходить авост (HALT).
В рапорте об Обероне же прямо сказано:
The Boolean expression preceding a statement is called its guard. The guards are evaluated in sequence of occurrence, until one evaluates to TRUE, whereafter its associated statement sequence is executed. If no guard is satisfied, the statement sequence following the symbol ELSE is executed, if there is one.
...
While statements specify repetition. If any of the Boolean expressions (guards) yields TRUE, the corresponding statement sequence is executed. The expression evaluation and the statement execution are repeated until none of the Boolean expressions yields TRUE.
То есть семантика этих операторов отличается.
ЗЫ. Кстати, сам Дейкстра отнюдь не гнушался делать вложенные циклы и циклы с условиями внутри, а вовсе не всегда заморачивался с циклом своего имени. Например:
x, y, z := X, Y, 1;
do y ≠ 0 → do 2 | y → x, y := x*x, y/2 od;
y, z := y − 1, z*x
od {R стало истинным}или
x, y, z := X, Y, 1;
do y<>0 → if non 2|y → y, z := y − 1, z*x
□ 2|y → пропустить fi;
x, y := x*x, y/2
odхотя, казалось бы, уж здесь-то самое ему (ЦД) место...
