Автор Тема: Инварианты к двум циклам  (Прочитано 34674 раз)

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 482
    • Просмотр профиля
Инварианты к двум циклам
« : Сентябрь 09, 2012, 03:04:59 pm »
Пароль к посту http://oberspace.dyndns.org/index.php/topic,253.msg6318.html#msg6318 : "ZRL/|EqEr<x<<Y" без кавычек.
Содержимое файла для удобства:
Цитировать
Инвариант для цикла Info21: в просмотренной области нет последовательности 00 и переменная oneZero  имеет значение: последний элемент просмотренной области есть 0.

Инвариант для цикла в последнем решении Александр Шостак: в переменной ChainLen лежит длина хвоста просмотренной области, состоящего из нулей.
В конце файла добавлен мусор, т.к. крошечный размер файла – сама по себе информация.
Если кто-нибудь ожидал увидеть полстраницы математических значков, то будет сильно огорчен.

Тексты программ для удобства:
Info21, http://forum.oberoncore.ru/viewtopic.php?p=72961#p72961
      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;

Александр Шостак, http://forum.oberoncore.ru/viewtopic.php?p=72958#p72958
CONST
  CHAIN_LEN   = 7;
  CHAIN_BYTE  = 0;

ChainLen  := 0;
i         := 0;

WHILE (i < LEN(a)) & (ChainLen < CHAIN_LEN) DO
  IF a[i] = CHAIN_BYTE THEN
    INC(ChainLen);
  ELSE
    ChainLen := 0;
  END;

 INC(i);
END;

Мой комментарий:

Info21 разъяснил нам про инвариант, что "он там тривиальный до бессодержательности.
Именно поэтому и не понадобился.
"
Так вот, в решении Александр Шостак инвариант почти такой же тривиальный (дополнение чуть ниже), но он ДРУГОЙ. Разные инварианты – разные программы. Углубляться дальше не буду.

А моя ошибка вот в чем: инвариант для решения  Александр Шостак не полон. Ниоткуда не следует, что найденный кусок будет первым от начала массива. Я заметил, да было уже поздно. Желающие могут попробовать сформулировать недостающую часть.

Кстати, я помню, что, по-моему, albobin записал решение Info21 по человечески, без всяких ЦД. Именно так оно бы и выглядело, если бы рождалось осмысленно. Но не нашел этого куска, неужели опять удалили?

DIzer

  • Гость
Re: Инварианты к двум циклам
« Ответ #1 : Сентябрь 09, 2012, 03:20:46 pm »
а что это за язык то:
while ... do
...
elsif .... do
...
end;

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 482
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #2 : Сентябрь 09, 2012, 03:23:44 pm »
Сэкономил на цитировании, забыл что тема может быть закрытой. У Info21 в начале
"Чтобы не казалось, что мой вариант сложнее, перепишу на Обероне-07, где ЦД есть явно:"

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #3 : Сентябрь 09, 2012, 03:37:10 pm »
а что это за язык то:
while ... do
...
elsif .... do
...
end;
В принципе похоже на Оберон-07, вот только ключевые слова почему-то в нижнем регистре...
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

DIzer

  • Гость
Re: Инварианты к двум циклам
« Ответ #4 : Сентябрь 09, 2012, 03:47:29 pm »
 а это уже я поленился - у Петра в сообщении они были в нормально регистре  :)

qp

  • Newbie
  • *
  • Сообщений: 28
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #5 : Сентябрь 09, 2012, 03:59:06 pm »
Инвариант для цикла Info21: в просмотренной области нет последовательности 00 и переменная oneZero  имеет значение: последний элемент просмотренной области есть 0.
Хмм, т.е. после окончания работы цикла инвариант не выполняется?

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #6 : Сентябрь 09, 2012, 04:33:38 pm »
Вообще, в той же "Дисциплине программирования" Дейкстра не стеснялся использовать ветвления и даже подциклы внутри главного цикла.
И если уж на то пошло, если делать этот цикл и правда по Дейкстре (с недетерменированным порядком вычисления охраняемых выражений), то должно быть так:
i, found := 0, false;
do i < len(a) - 1 and not found ->
  x, y := a[i], a[i+1];
  if x = 0 and y = 0 -> found := true
  [] x ≠ 0 or  y ≠ 0 -> i := i + 1
  fi
od
Полистал я Дейкстрову книшку и уверен, что этот вариант самый что ни на есть "по Дейкстре" ))
Вариант, правда, не очень эффективный, но зато простейший и очевидный.
И похож на мой вариант на хаскелле:
find00 xs = find xs 0
  where
    find (0:0:_) n = Just n
    find (_:xs)  n = find xs (n+1)
    find []      _ = Nothing
« Последнее редактирование: Сентябрь 09, 2012, 04:37:25 pm от Geniepro »
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #7 : Сентябрь 09, 2012, 04:53:43 pm »
И если уж на то пошло, если делать этот цикл и правда по Дейкстре (с недетерменированным порядком вычисления охраняемых выражений)

По поводу недетерменированности -- цитата из Дейкстры:
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 482
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #8 : Сентябрь 09, 2012, 05:02:09 pm »
Инвариант для цикла Info21: в просмотренной области нет последовательности 00 и переменная oneZero  имеет значение: последний элемент просмотренной области есть 0.
Хмм, т.е. после окончания работы цикла инвариант не выполняется?
Выполняется. Если расписывать аккуратно, то просмотренная область - это элементы с индексами j: 0<=j<i.
Но я этого обычно не делаю.

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 482
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #9 : Сентябрь 09, 2012, 05:29:00 pm »
Вообще, в той же "Дисциплине программирования" Дейкстра не стеснялся использовать ветвления и даже подциклы внутри главного цикла.
И если уж на то пошло, если делать этот цикл и правда по Дейкстре (с недетерменированным порядком вычисления охраняемых выражений), то должно быть так:
i, found := 0, false;
do i < len(a) - 1 and not found ->
  x, y := a[i], a[i+1];
  if x = 0 and y = 0 -> found := true
  [] x ≠ 0 or  y ≠ 0 -> i := i + 1
  fi
od
Полистал я Дейкстрову книшку и уверен, что этот вариант самый что ни на есть "по Дейкстре" ))
Вариант, правда, не очень эффективный, но зато простейший и очевидный.
Действительно, это первое, что приходит в голову (мне, во всяком случае). Но, конечно не так, а вот так:
i:= 0;
do
  i < len(a) - 1 and (a[i] <>0 or a[i+1]<>0) -> i:=i+1;
od
Очень неэффективно и не расширяемо на более длинную цепочку нулей.

Первый вопрос который я задал vlad'у в той теме был об этом варианте: "Что значит "правильным". Лишнее сравнение в случае массива - это правильно?" http://oberspace.dyndns.org/index.php/topic,253.msg6087.html#msg6087

Geniepro, осталось сформулировать инвариант для этого цикла...

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #10 : Сентябрь 09, 2012, 06:03:55 pm »
Geniepro, осталось сформулировать инвариант для этого цикла...
Зачем формулировать инварианты заведомо правильных циклов? Делать ради самого делания? о_О
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #11 : Сентябрь 09, 2012, 06:09:35 pm »
Действительно, это первое, что приходит в голову (мне, во всяком случае). Но, конечно не так, а вот так:
i:= 0;
do
  i < len(a) - 1 and (a[i] <>0 or a[i+1]<>0) -> i:=i+1;
od
Тогда надо добавить в конце строчку:
found := i < len(a)
если хотим получить ещё и признак того, нашли эти два нуля или нет...
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #12 : Сентябрь 09, 2012, 06:28:58 pm »
Тогда надо добавить в конце строчку:
found := i < len(a)
если хотим получить ещё и признак того, нашли эти два нуля или нет...
точнее
found := i < len(a) - 1

Вот, без тестирования ошибку уже найти труднее, чем в моём варианте )))
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

albobin

  • Full Member
  • ***
  • Сообщений: 198
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #13 : Сентябрь 10, 2012, 04:05:54 am »
Инвариант для цикла Info21: в просмотренной области нет последовательности 00 и переменная oneZero  имеет значение: последний элемент просмотренной области есть 0.
Инвариант с2-мя изъянами неточности, на что уже указал qp в http://oberspace.dyndns.org/index.php/topic,331.msg8786.html#msg8786
В такой формулировке инвариант не выполняется по выходу из цикла в случае нахождения 00.
Кстати, я помню, что, по-моему, albobin записал решение Info21 по человечески, без всяких ЦД. Именно так оно бы и выглядело, если бы рождалось осмысленно. Но не нашел этого куска, неужели опять удалили?
Нет, я ничего не переписывал. Было когда-то дело, но там был цикл , кажется Ильи Ермакова (могу ошибаться), с полным перебором.



albobin

  • Full Member
  • ***
  • Сообщений: 198
    • Просмотр профиля
Re: Инварианты к двум циклам
« Ответ #14 : Сентябрь 10, 2012, 04:13:05 am »
Инвариант для цикла Info21: в просмотренной области нет последовательности 00 и переменная oneZero  имеет значение: последний элемент просмотренной области есть 0.
Хмм, т.е. после окончания работы цикла инвариант не выполняется?
Выполняется. Если расписывать аккуратно, то просмотренная область - это элементы с индексами j: 0<=j<i.
Но я этого обычно не делаю.
Как бы не расписывали, найти 00 можно только в просмотренной области  :)