Цикл Дейкстры

В классической работе A Discipline of Programming, Prentice-Hall, 1976 (русский перевод: Дейкстра Э. Дисциплина программирования. М: Мир, 1978) Эдсгер Дейкстра (E.W. Dijkstra) ввёл "многоветочный" вариант цикла WHILE, обосновав его в своей теории систематического вывода императивных программ. Этот цикл может оказаться удобным для выражения и верификации алгоритмов, обычно записываемых через вложенные циклы. Должны снижаться и усилия по отладке. Однако до недавнего времени ни один язык программирования не поддерживал цикла Дейкстры в явном виде - пока не появился Оберон-07 (N. Wirth. The Programming Language Oberon. Revision 1.9.2007).

Синтаксис цикла Дейкстры на Обероне определяется следующим правилом:

WhileStatement
 = WHILE логическое выражение DO
      последовательность операторов
   {ELSIF логическое выражение DO
      последовательность операторов}
END.

Если вычисление любого из логических выражений (охран) дает TRUE, то выполняется соответствующая последовательность операторов. Вычисление охран и выполнение соответствующих последовательностей повторяется до тех пор, пока все охраны не будут давать FALSE. Таким образом, постусловием для этого цикла является конъюнкция (логическое "и") отрицаний всех охран.

Пример:

WHILE m > n DO 
 m := m - n
 ELSIF n > m DO n := n - m
END

Постусловие: ~(m > n) & ~(n > m), что эквивалентно n = m.

Инвариант цикла должен выполняться в начале и в конце каждой ветви.

Грубо говоря, n-веточный цикл Дейкстры соответствует конструкциям из n обычных циклов, каким-то образом вложенных друг в друга.

Удобство цикла Дейкстры обусловлено тем, что вся логика сколь угодно сложного цикла выводится на один уровень и проясняется, причём алгоритмы с разными случаями запутанных циклов трактуются единообразно.

Эффективный способ построения такого цикла состоит в том, чтобы перечислять все возможные ситуации, которые могут возникнуть, описывая их соответствующими охранами, и для каждой из них независимо от остальных строить операции, обеспечивающие продвижение по данным, вместе с операциями, обеспечивающими восстановление инварианта. Перечисление ситуаций заканчивается, когда дизъюнкция (логическое или) всех охран покроет предполагаемое предусловие цикла. При этом задача корректного построения цикла облегчается, если отложить беспокойство о порядке вычисления охран и выполнения ветвей, экономии операций при вычислении охран и т.п. до тех пор, пока цикл не будет корректно построен. Такие мелкие оптимизации редко по-настоящему важны, а их реализация сильно облегчается, когда корректность сложного цикла уже обеспечена. В теории Дейкстры последовательность выбора ветвей цикла и вычисления соответствующих охран не определена, но проще всего предположить, что охраны вычисляются в текстуальном порядке.

Во многих языках программирования цикл Дейкстры нужно специально моделировать. В процедурных языках, например, в старых версиях Оберона, включая Компонентный Паскаль, для этого подойдёт цикл LOOP, тело которого состоит из многоветочного условного оператора с оператором выхода в ветке ELSE:

LOOP IF логическое выражение THEN
  последовательность операторов
{ELSIF логическое выражение THEN
  последовательность операторов}
 ELSE EXIT END 
END.

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

Приведём для сравнения 2 реализации простого алгоритма построчного вывода элементов матрицы на экран (Паскаль). В первом листинге применён классический вложенный цикл:

const a:array [1..3,1..3] of integer = (
 (1,2,3),
 (4,5,6),
 (7,8,9)
);
var i,j:integer;
begin
 for i:=1 to 3 do begin
  writeln;
  for j:=1 to 3 do write (a[i,j],' ');
 end;
end.

Второе решение выполнено (хотя и несовершенно) "в стиле Дейкстры":

const a:array [1..3,1..3] of integer = (
 (1,2,3),
 (4,5,6),
 (7,8,9)
);
var i,j:integer;
begin
 i:=1; j:=1;
 repeat
  write (a[i,j],' ');
  if j<3 then inc(j)
  else if i<3 then begin writeln; inc(i); j:=1; end
  else break;
 until false;
end.

Думаю, можно признать, что цикл Дейкстры способен как усложнить программирование простой задачи, так и облегчить программирование сложной :) Хорошее обсуждение есть вот здесь.

31.03.2013, 15:33 [12337 просмотров]