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

[DIzer]

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

Инвариант цикла должен подсказывать логику работы цикла.
Утверждения вроде "2*2=4" или "Волга впадает в Каспийское море" никак не подсказывают нам свойств цикла, а значит и не являются инвариантами цикла.
Да, эти утверждения являются инвариантами, но не цикла...

Никто никому не должен - есть четкое определение инварианта (по которому можно определить является ли  ПРОИЗВОЛЬНОЕ логическое  выражение оным), есть примеры  примененя методы- в основной  своей массе  на таких циклах где формулировка инвариантов скорее в тягость, есть ОСТОРОЖНЫЕ высказывания МЭТРОВ (Дейкстры, Грисома) по данной методе- а есть танцульки вокруг "идола" в коровне , в основе которой манипуляция с естественным желанием человека получить все с наименьшими затратами, ну  . и есть Петр Алмазов...

[Geniepro]

Вариант от info21 (псевдоцикл Дейкстры)

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

i := 0;
oneZero := FALSE; (*oneZero = перед i стоит нуль*)
WHILE (i < LEN(a)) & ~oneZero DO
    oneZero := a[i] = 0;
    INC(i);
ELSIF (i < LEN(a)) & (a[i] # 0) DO
    oneZero := FALSE;
    INC(i);
END;плох тем, что оставляет неверное представление о настоящем цикле Дейкстры.

Вообще я попробовал сделать этот алгоритм в виде цикла Дейкстры, но что-то сомневаюсь, что из этого выйдет что-то путное -- ну не подходит этот алгоритм для ЦД. Вот что реально из себя представляет алгоритм, представленный info21:

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

i     := 0;
found := FALSE; (* found = (a[i-1] = 0) & (a[i] = 0) *)
WHILE (i < LEN(a)) & ~found DO
   WHILE (i < LEN(a)) & a[i] # 0 DO   INC(i) END;
   IF    (i < LEN(a)) & a[i] # 0 THEN INC(i)
   ELSE                               found := TRUE
   END;
END;

[albobin]

Вот что реально из себя представляет алгоритм, представленный info21:

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

i     := 0;
found := FALSE; (* found = (a[i-1] = 0) & (a[i] = 0) *)
WHILE (i < LEN(a)) & ~found DO
   WHILE (i < LEN(a)) & a[i] # 0 DO   INC(i) END;
   IF    (i < LEN(a)) & a[i] # 0 THEN INC(i)
   ELSE                               found := TRUE
   END;
END;

Да ну?

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

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


[Geniepro]

Вот что реально из себя представляет алгоритм, представленный info21:

Таки ошибся, вот правильный вариант:

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

i     := 0;
found := FALSE; (* found = (a[i-1] = 0) & (a[i] = 0) *)
WHILE (i < LEN(a)) & ~found DO
    WHILE (i < LEN(a)) & a[i] # 0 DO INC(i) END;
    INC(i);
    IF (i < LEN(a)) THEN
        IF a[i] = 0 THEN found := TRUE
        ELSE             INC(i)
        END
    END
END;

[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;

Это не мой вариант - это суть варианта от info21

[Geniepro]

Это не мой вариант - это суть варианта от info21

Логически да, но вычислительная сложность всё-таки разная.

[Peter Almazov]

А можно объяснить такой ниграмытной быдле как я, какой собственно профит от этих "формальных" методов в императивных языках общего назначения?

Вот здесь http://oberspace.dyndns.org/index.php/topic,261.msg6309.html#msg6309 я уже предлагал всем желающим сделать 2 упражнения.

Отношение к ним может быть разное.

Некто может сказать:
"Что за херня? Я не могу уверенно, быстро и без ошибок написать цикл длиной порядка 10 строк, при том, что общая идея мне ясна. Не мудак ли я?
Хочу перезжать подобные задачи как трактор."

Другой может сказать:
"Все это – х@$#я"
"Программист с такими циклами не встретится" (c) И.Е.Ермаков
"Я посмотрю в справочнике"
"Я использую библиотечную сортировку"
"Я покрою все тестами"
и т. п.

Тут уж каждый сам выбирает

[DIzer]

А можно объяснить такой ниграмытной быдле как я, какой собственно профит от этих "формальных" методов в императивных языках общего назначения?

Вот здесь http://oberspace.dyndns.org/index.php/topic,261.msg6309.html#msg6309 я уже предлагал всем желающим сделать 2 упражнения.

Отношение к ним может быть разное.

Некто может сказать:
"Что за херня? Я не могу уверенно, быстро и без ошибок написать цикл длиной порядка 10 строк, при том, что общая идея мне ясна. Не мудак ли я?
Хочу перезжать подобные задачи как трактор."

Другой может сказать:
"Все это – х@$#я"
"Программист с такими циклами не встретится" (c) И.Е.Ермаков
"Я посмотрю в справочнике"
"Я использую библиотечную сортировку"
"Я покрою все тестами"
и т. п.

Тут уж каждый сам выбирает

может ... может да , может нет.... может быть, может не быть... а где ответ то на вопрос==частное мнение "познавшего дзен" ? 

[albobin]

Это не мой вариант - это суть варианта от info21

Логически да, но вычислительная сложность всё-таки разная.

То есть Ваш вариант того,

что реально из себя представляет алгоритм, представленный info21:

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

i     := 0;
found := FALSE; (* found = (a[i-1] = 0) & (a[i] = 0) *)
WHILE (i < LEN(a)) & ~found DO
    WHILE (i < LEN(a)) & a[i] # 0 DO INC(i) END;
    INC(i);
    IF (i < LEN(a)) THEN
        IF a[i] = 0 THEN found := TRUE
        ELSE             INC(i)
        END
    END
END;остаётся в силе ?

[Geniepro]

То есть Ваш вариант того,

что реально из себя представляет алгоритм, представленный info21:

...
остаётся в силе ?

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

[albobin]

Тревожно как-то от таких аналогий 

[Geniepro]

Тревожно как-то от таких аналогий 

В Обероне-07 оператор

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

WHILE cond1 DO s1
ELSIF cond2 DO s2
ELSIF cond3 DO s3
...
ELSIF condN DO sN
ENDэквивалентен конструкции

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

LOOP
    WHILE cond1 DO   s1 END;
    IF    cond2 THEN s2
    ELSIF cond3 THEN s3
    ...
    ELSIF condN THEN sN
    ELSE  EXIT
    END
END
Берём алгоритм info21

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

i := 0;
oneZero := FALSE;
WHILE (i < LEN(a)) & ~oneZero DO
    oneZero := a[i] = 0;
    INC(i)
ELSIF (i < LEN(a)) & (a[i] # 0) DO
    oneZero := FALSE;
    INC(i)
END;и преобразуем его по этой схеме в:

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

i := 0;
oneZero := FALSE;
LOOP
    WHILE (i < LEN(a)) & ~oneZero DO
        oneZero := a[i] = 0;
        INC(i)
    END;
    IF (i < LEN(a)) & (a[i] # 0) THEN
        oneZero := FALSE;
        INC(i)
    ELSE
        EXIT
    END
ENDДалее избавляемся от выхода из середины:

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

i := 0;
oneZero := FALSE;
b := TRUE;
WHILE b
    WHILE (i < LEN(a)) & ~oneZero DO
        oneZero := a[i] = 0;
        INC(i)
    END;
    IF (i < LEN(a)) & (a[i] # 0) THEN
        oneZero := FALSE;
        INC(i)
    ELSE
        b := FALSE
    END
ENDизбавляемся от лишнего флажка oneZero:

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

i := 0;
not_found := TRUE;
WHILE (i < LEN(a)) & not_found
    WHILE (i < LEN(a)) & (a[i] # 0) DO
        INC(i)
    END;
    INC(i);
    IF (i < LEN(a)) THEN
        IF a[i] # 0 THEN
            INC(i)
        ELSE
            not_found := FALSE
        END
    END
ENDВыбирайте, какой Вам больше по душе...

[ilovb]

Тревожно как-то от таких аналогий 

В Обероне-07 оператор

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

WHILE cond1 DO s1
ELSIF cond2 DO s2
ELSIF cond3 DO s3
...
ELSIF condN DO sN
ENDэквивалентен конструкции

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

LOOP
    WHILE cond1 DO   s1 END;
    IF    cond2 THEN s2
    ELSIF cond3 THEN s3
    ...
    ELSIF condN THEN sN
    ELSE  EXIT
    END
END

Не понял... почему такой?

Зачем там while?

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

LOOP
    IF    cond1 THEN s1
    ELSIF cond2 THEN s2
    ELSIF cond3 THEN s3
    ...
    ELSIF condN THEN sN
    ELSE  EXIT
    END
END

[Geniepro]

Не понял... почему такой?
Зачем там while?

Это простейшая оптимизация.
Пока условие cond1 истинно, выполняться в цикле будет s1.
С другими охранными выражениями такой оптимизации сделать не получится...

Я имею в виду, что в такой вид этот псевдо-ЦД переводят компиляторы сей и компилятор Оберона-07М от Рифата...