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

[albobin]

"в просмотренной части последовательности нет 00". Прежде чем объяснять в четвертый раз, у меня большая просьба к albobin (на других надежды нет) ...   Может, и объяснять ничего не придется.

По поводу "просмотренной части последовательности".  Придирка ведь носит несколько стёбовый характер. Конечно все понимают, что говоря о "просмотренном" имеют ввиду множество всех переменных цикла при которых был вход в тело цикла.  Но c другой стороны,  не "посмотремши" на элемент массива, сложновато использовать его значение в логических условиях.     
 PS.
Извините великодушно, но выполнить просьбу не могу - высочайшего уровня скромность не позволяет

[Geniepro]

Прежде чем объяснять в четвертый раз, у меня большая просьба к albobin (на других надежды нет), попробуйте сформулировать инвариант для этого цикла.

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

i:= 0;
do
  i < len(a) - 1 and (a[i] <>0 or a[i+1]<>0) -> i:=i+1;
od
Может, и объяснять ничего не придется.

Так я же вроде сформулировал: http://oberspace.dyndns.org/index.php/topic,331.msg8824.html#msg8824
Или у меня там где-то ашыпка?

[Peter Almazov]

Конечно все понимают, что говоря о "просмотренном" имеют ввиду множество всех переменных цикла при которых был вход в тело цикла.

Я не знаю, что все понимают и имеют ввиду.
Пока я вижу, что никто ни х@$% не понимает (кроме Info21).

Инвариант этого цикла: "в просмотренной части последовательности нет 00".

Вот это кто писал, двойник что-ли:

Для циклов поиска, наверное самый естественный инвариант - это отсутствие "искаемого" в текущем просмотренном:)
PS.
Под "просмотренным" понимается "до текущей точки(исключительно)"

[DIzer]

что касается вашего виденья, Петр - по ссылке которую вы не постеснялись здесь дать  - я  привел  там вам еще пару инвариантов (по определению) и попросил прокомментировать их
- у вас КИШКА ТОНКА ОКАЗАЛАСЬ - ответ  сводился "рассуждения долгие и нудные , у меня нет времени на это", кроме того, Албобин нашел у вас ошибку (это свидетельство  что эта метода даже вам(ее адепту) не помогла ее избежать- если это так то НАХ. данная методика? и не е.-те другим мозги...

Сколько пафоса. Может, не надо было сразу так, большими буквами-то.
Можно было и помягше: "Тема все еще представляет интерес". А то я исхожу из худшего – что надоел уже всем повторением одно и того же.

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

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

i:= 0;
do
  i < len(a) - 1 and (a[i] <>0 or a[i+1]<>0) -> i:=i+1;
od
Может, и объяснять ничего не придется.

  Пафоса ,Петр до х.. у вас (когда - затевали этот балаган, и если вы обвиняете коровят и в незнании топика - будьте добры показать свою квалификацию, а то есть ОЧЕНЬ большая вероятность обокакаться как недавно Инфо21 обратившись с прямым вызовом к участникам этого форума...)- а вот знаний ответить четко на поставленный вопрос (как мой , так и Ильи) - ни х.. - и этот ответ лишний раз подтверждает это...

[Peter Almazov]

Не спешите, интересно, что albobin напишет.

[DIzer]

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

[valexey_u]

Не спешите, интересно, что albobin напишет.

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

[DIzer]

Не спешите, интересно, что albobin напишет.

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

Это я так понимаю ... вопрос к Петру ? 

[valexey_u]

Это я так понимаю ... вопрос к Петру ? 

Да, конечно. Я ведь именно его процитировал.

Но если кто-то другой, познавший дзен, мне толково объяснит, то я не погнушаюсь.

[albobin]

Вот это кто писал, двойник что-ли:

Для циклов поиска, наверное самый естественный инвариант - это отсутствие "искаемого" в текущем просмотренном:)
PS.
Под "просмотренным" понимается "до текущей точки(исключительно)"

Нет не двойник.
Всё так и есть, если в общем рассматривать инвариант циклов поиска, но есть ещё же и частные конкретные случаи  в которых этот инвариант принимает другие формы выражения той же самой сути.
Рискую поумничать, но выражу своё или скорее всего где то прочитанное  и переваренное или перевранное  в мозгах представление о сути цикла поиска.
Есть некий предикат определённый на некотором конечном множестве последовательных целых чисел. Поиск определяем как простой перебор чисел по возрастанию до того момента когда предикат примет значение истины.
Вышли за пределы  - ничего не найдено.
Вот и инвариант цикла как раз и будет :  значение предиката ложь при всех значениях до текущего.
Главное что есть последовательный перебор и отсутствие препятствий к достижению конца последовательности кроме как ограничения не нарушать инвариант. Вот и всё.   

[Peter Almazov]

Одни забывают про инвариант, другие про охрану. Не надо ничего перевирать, читайте первоисточники или, накрайняк, это http://oberspace.dyndns.org/index.php/topic,253.msg6224.html#msg6224

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

Для цикла Дейкстры –
Инвариант И (конъюнкция отрицаний охран)

После упомянутого выше цикла будет истинно:

("в просмотренной части последовательности нет 00") И ((i вышло за границы) ИЛИ (впереди стоят два нуля))

Первым делом после цикла (допустим, нашли 00) мы разбираемяся с i, как верно заметил Geniepro здесь http://oberspace.dyndns.org/index.php/topic,331.msg8796.html#msg8796

Не вышло i за границы, значит верно, что:
("в просмотренной части последовательности нет 00") И (впереди стоят два нуля)
Мы гарантируем, что нашли первые от начала 00, о чем многие забывают.

После цикла Info21 и разбирательства с i останется:
(в просмотренной области нет последовательности 00 и последний элемент просмотренной области есть 0) И (впереди стоит 0).

Прошу заметить, что здесь нет никакой (страшной) математики, единственное, что надо знать твердо - это законы де Моргана.

[Peter Almazov]

Теперь по поводу инвариантов от Dizer. Я не зря спросил про множество всех истинных утверждений, все они будут инвариантами цикла.
Процитирую Гриса, стр. 149:

У цикла имеется много инвариантов. Например, предикат x*0=0 является инвариантом любого цикла, так как он всегда истинен. Но инварианты, удовлетворяющие условиям теоремы (11.6), способствуют пониманию цикла и поэтому важны.

Слово "теорема" пугает народ (и меня тоже, да). Там речь идет ровно о том, что я написал в начале: после выполнения цикла будет истинным выражение
Инвариант И (НЕ охрана цикла)

Поэтому толку от инвариантов типа "Волга впадает в Каспийское море" будет маловато.

[DIzer]

Теперь по поводу инвариантов от Dizer. Я не зря спросил про множество всех истинных утверждений, все они будут инвариантами цикла.
Процитирую Гриса, стр. 149:

У цикла имеется много инвариантов. Например, предикат x*0=0 является инвариантом любого цикла, так как он всегда истинен. Но инварианты, удовлетворяющие условиям теоремы (11.6), способствуют пониманию цикла и поэтому важны.

Слово "теорема" пугает народ (и меня тоже, да). Там речь идет ровно о том, что я написал в начале: после выполнения цикла будет истинным выражение
Инвариант И (НЕ охрана цикла)

Поэтому толку от инвариантов типа "Волга впадает в Каспийское море" будет маловато.

   ну ладно , хоть Гриса приплели.... хотя я  дал вам не тривиальный инвариант... а мог бы дать и более сложную комбинацию элементарных (и не очень) функций от параметров входящих в цикл.. И ОНИ БЫЛИ БЫ ТАКЖЕ ЕГО НЕ ТРИВИАЛЬНЫМИ ИНВАРИАНТАМИ - ПОЭТОМУ ваши закидоны о "правильности" инварианта ничего не стоят без ТОЧНОГО  и КОНСТРУКТИВНОГО определения тех из них по которым можно определить цикл, И ГЛАВНОЕ - ЭФФЕКТИВНОГО способа ИХ КОНСТРУИРОВАНИЯ в общем случае. Вот когда дадите его - тогда и будем сравнивать эффективность этой методы... Да и насчет цитаты      - вам не кажется что Григс - в отличие от вас и коровят использует НА ПОРЯДОК более расплывчато неопределенные  высказывания - "способствуют пониманию цикла и поэтому важны" ? с чего бы это? - может потому, что он , в отличие от вас понимает, что данная метода не ПАНАЦЕЯ?

[albobin]

Вот и всё.

Нет не всё. Подумавши ещё немного, ворочаясь от бессонницы ( в другое время как-то нужды нет) , пришёл к выводу, что  в том, что здесь обсуждается и в том, что и я написал в предыдущем послании, насчёт инварианта в той формулровке цикла поиска, есть изъян - хрень масло-маслянная. 
А правда вся в том, что говорил info21 в http://forum.oberoncore.ru/viewtopic.php?f=82&t=3770&start=20#p72977 инвариант тут "тривиальный до бессодержательности"
Вот есть массив a[] длины N , нужно найти первый нулевой элемент

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

i:=0; while (i<N)&(a[i]<>0) do i:=i+1 end
Более правильная формулировка задачи такая: найти минимальное значение i  при котором  предикат

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

a[i]=0 будет иметь значение истина. Для решения этой задачи мы выбираем  такой способ упорядочения проверяемых элементов массива при котором каждый следующий i больше предыдущего и ни один i из диапазона от 0 до N-1 не должен быть пропущен, а это есть то, что следующее значение i должно быть больше предыдущего на единицу, а начальное значение должно быть 0. Вот здесь и настоящий "тривиальный" инвариант.
i+1=i+1

 

[Geniepro]

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

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