Инварианты к двум циклам

[Kemet]

В цикде Дейкстры, вроде как, каждая ветка (охрана) открывает (если условие истинно) точку входа (и только одну, даже если истинны несколько охран) для следующей итерации.

[albobin]

Выбирайте, какой Вам больше по душе...

Код: [Выделить]

WHILE (i < LEN(a)) & (~oneZero OR a[i] # 0)   DO   oneZero := a[i] = 0; INC(i) END;


[ilovb]

Надо просто усвоить, что после выполнения цикла будет истинным выражение
Инвариант И (НЕ охрана цикла)
Для цикла Дейкстры –
Инвариант И (конъюнкция отрицаний охран)

И это все? 

А кто пишет циклы иначе? Или вся соль в том, чтобы инвариант и охрана обязательно явно были в условии цикла?

[Peter Almazov]

До меня только недавно дошло, что термин "просмотренная область" может сильно сбивать с толку. Гораздо уместнее было бы "обработанная область".
Хотя я дал формальное определение, но с точки зрения русского языка получается туфта: имеем "просмотренную область" и рядом один или два элемента, которые мы просмотрели и увидели равны они 0 или нет.
С термином "обработанная область" такой коллизии не возникло бы.

Приношу свои извинения.

[Geniepro]

В цикле Дейкстры, вроде как, каждая ветка (охрана) открывает (если условие истинно) точку входа (и только одну, даже если истинны несколько охран) для следующей итерации.

При этом порядок выполнения веток ЦД не детерминирован.
Но речь-то не про цикл Дейкстры, а про оператор WHILE-ELSIF-END в Обероне-07. В этом обероновском псевдо-ЦД порядок веток определён -- сверху вниз...

[Geniepro]

Выбирайте, какой Вам больше по душе...

Код: [Выделить]

WHILE (i < LEN(a)) & (~oneZero OR a[i] # 0)   DO   oneZero := a[i] = 0; INC(i) END;


Но почему же не

Код: [Выделить]

WHILE (i < LEN(a)-1) & (a[i] # 0 OR a[i+1] # 0) DO INC(i) END;

[albobin]

Выбирайте, какой Вам больше по душе...

Код: [Выделить]

WHILE (i < LEN(a)) & (~oneZero OR a[i] # 0)   DO   oneZero := a[i] = 0; INC(i) END;


Но почему же не

Код: [Выделить]

WHILE (i < LEN(a)-1) & (a[i] # 0 OR a[i+1] # 0) DO INC(i) END;

1.потому что речь идет о варианте от info21, значит
2.потому что та строка, что Вы предлагаете не эквивалентна исходному циклу. (В исходном - или вышли за пределы или i указывает на конец 00, а в здесь - на начало)
3.потому что мне по душе больше условие   i<LEN(a) .  Вышли за пределы - значит не нашли в пределах.

[albobin]

Но почему же не

Код: [Выделить]

WHILE (i < LEN(a)-1) & (a[i] # 0 OR a[i+1] # 0) DO INC(i) END;

1.потому что речь идет о конкретном варианте от info21
2.потому что та строка, что Вы предлагаете не эквивалентна исходному циклу. (В исходном - или вышли за пределы или i указывает на конец 00, а в здесь - на начало)
3.потому что мне по душе больше условие   i<LEN(a) .  Вышли за пределы - значит не нашли в пределах.

[Geniepro]

Но почему же не

Код: [Выделить]

WHILE (i < LEN(a)-1) & (a[i] # 0 OR a[i+1] # 0) DO INC(i) END;

1.потому что речь идет о конкретном варианте от info21
2.потому что та строка, что Вы предлагаете не эквивалентна исходному циклу. (В исходном - или вышли за пределы или i указывает на конец 00, а в здесь - на начало)
3.потому что мне по душе больше условие   i<LEN(a) .  Вышли за пределы - значит не нашли в пределах.

Зато мой вариант более наглядно показывает суть того, что делает этот цикл ))

[ilovb]

Или вся соль в том, чтобы инвариант и охрана обязательно явно были в условии цикла?

Типа переписываю это:
http://oberspace.dyndns.org/index.php/topic,253.msg6133.html#msg6133
так:

Процедура КнопкаВыполнитьНажатие(Кнопка)
   
   Массив = Новый Массив;
   Массив.Добавить(1);
   Массив.Добавить(0);
   Массив.Добавить(1);
   Массив.Добавить(0);
   Массив.Добавить(1);
   Массив.Добавить(0);
   Массив.Добавить(0);
   
   Граница = Массив.ВГраница();
   ТекущийИндекс = 0;
     
   Пока ТекущийИндекс < Граница И НЕ (Массив[ТекущийИндекс] = 0 И Массив[ТекущийИндекс + 1] = 0) Цикл
     
      ТекущийИндекс = ТекущийИндекс + 1;
           
   КонецЦикла;
   
   Если ТекущийИндекс < Граница И Массив[ТекущийИндекс] = 0 И Массив[ТекущийИндекс + 1] = 0 Тогда
      Сообщить(ТекущийИндекс);
   Иначе
      Сообщить("Хрен");
   КонецЕсли;
   
КонецПроцедуры

... и все становится по науке?

[DIzer]

... и все становится по науке?

неплохо ... сказано 

[albobin]

Зато мой вариант более наглядно показывает суть того, что делает этот цикл ))

Тогда уж так чтоб не придираться

Код: [Выделить]

i:=2; WHILE (i < LEN(a) & (a[i-1] # 0 OR a[i] # 0)) DO INC(i) END; j
одну скобку ) я тоже пропустил

[Geniepro]

Типа переписываю это:
http://oberspace.dyndns.org/index.php/topic,253.msg6133.html#msg6133
так:
...
... и все становится по науке?

Если в 1С нумерация элементов массива идёт с 0 до (Массив.ВГраница()-1), то видимо надо сделать так:
Граница = Массив.ВГраница() - 1;

[Geniepro]

Зато мой вариант более наглядно показывает суть того, что делает этот цикл ))

Тогда уж так чтоб не придираться

Код: [Выделить]

i:=2; WHILE (i < LEN(a) & (a[i-1] # 0 OR a[i] # 0)) DO INC(i) END;

Если нумерация элементов массива идёт с нуля, то такой вариант не обнаружит два нуля в самом начале массива -- первый элемент массива вообще не будет просмотрен.

[albobin]

Зато мой вариант более наглядно показывает суть того, что делает этот цикл ))

Тогда уж так чтоб не придираться

Код: [Выделить]

i:=2; WHILE (i < LEN(a) & (a[i-1] # 0 OR a[i] # 0)) DO INC(i) END;

Если нумерация элементов массива идёт с нуля, то такой вариант не обнаружит два нуля в самом начале массива -- первый элемент массива вообще не будет просмотрен.

Да, конечно i:=1; ...
Я имел ввиду 2-й элемент массива
Привык, понимаете, с единицы считать