OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Вторник, 19 Март, 2024 14:11

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 55 ]  На страницу Пред.  1, 2, 3  След.
Автор Сообщение
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Понедельник, 04 Июнь, 2012 21:49 

Зарегистрирован: Четверг, 23 Апрель, 2009 18:01
Сообщения: 219
Для меня ЦД слишком запутывает логику простого обхода с подсчётом. Чуть измените задачу: нужно 3 нуля найти подряд или 7 единиц. Разницы нет на мой субъективный взгляд.
(ChainLen - длина цепочки.)

Код:
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;


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Понедельник, 04 Июнь, 2012 22:45 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Александр Шостак писал(а):
Разницы нет на мой субъективный взгляд.
Я о том же.

Но одна разница, все-таки, есть, которая проявится в более сложных случаях.
ЦД был написан формально, хотя и влёт, и он на корню верифицированный.
В чуть более сложных случаях "интуитивный подход" (или рукосуйство, кому как нравится) создаст проблемы.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Понедельник, 04 Июнь, 2012 22:55 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Info21 писал(а):
Чтобы не казалось, что мой вариант сложнее, перепишу на Обероне-07, где ЦД есть явно:
Код:
      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;

Рукосуи, не понимающие, с чем "едят" ЦД (это про альтернативно удаленных), не въезжают, что конъюнкция отрицаний охран сразу доказывает корректность цикла:

(i >= LEN(a)) OR (oneZero & (a[i]=0))

И даже не понимают, что это ("сразу дает ...") важно.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 05 Июнь, 2012 10:19 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
А ежели кому чисто структурно непонятна логика (напр., учням, которых ещё надо отучать от интуитивности) - можно, думаю, представить структуру маршрутов как устремлённый граф... (ессно, не забывая правильно разметить его остальным текстом :))...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 05 Июнь, 2012 10:31 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Альтернативные рукосуи продолжают пыхать злобой, пытаясь оправдать своё дремучее невежество (незнание элементарных основ формальных методов вообще и формальной логики в частности).
Пусть смотрят в школьной версии ББ два цикла -- прямой проход и обратный -- занимающихся трансляцией ключевых слов с нац. языка в английский, а потом обратно.

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

Они сразу заработали правильно, без отлладки.
Сразу.
Без отладки.

-----
Пардон, соврал насчёт никого: есть Trurl, светлая голова.


Последний раз редактировалось Info21 Вторник, 05 Июнь, 2012 11:14, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 05 Июнь, 2012 10:35 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Все эти мрачные диспуты приводят на ум такую аналогию (если кто придумает попроще, чтоб было доступно тем, кто не знает матанализа, было бы полезно).

Вот есть матанализ.
Это формализм такой брать производные и интегралы.
Все физмат-инженерные специальности должны его просто выучить, задач определенное количество отрешать, загнать в спинной мозг -- и больше никогда о нужности матанализа не задумываться.

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

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

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

С другой стороны, понятно, что индивиду после 25 лет вбить что-то существенно новое в голову можно обычно только рельсом. И то успех не гарантирован.

Так что пусть будут альтернативные форумы. Могилы для горбатых.

А силы тратить имеет смысл на образование молодняка.


Последний раз редактировалось Info21 Вторник, 05 Июнь, 2012 11:28, всего редактировалось 3 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 05 Июнь, 2012 10:41 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Забавно, что человек, претендующий на улучшение Оберона, облажался на некорректном окончании примитивного цикла.

А сколько слюны тут и там было разбрызгано.

Мракобесы.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 05 Июнь, 2012 16:35 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3261
Откуда: Астрахань
Спасибо за обоснование - буду приводить учням в качестве примера.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 05 Июнь, 2012 22:01 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Еще бы Питеру Алмазову про инвариант объяснить ... у меня сил нет.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Среда, 06 Июнь, 2012 07:33 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Info21 писал(а):
Все эти мрачные диспуты приводят на ум такую аналогию (если кто придумает попроще, чтоб было доступно тем, кто не знает матанализа, было бы полезно).
...
Попробую... хотя ясно, что не упоминать матанализа практически невозможно - но для не знающих можно постараться употребить лишь как понятие, не требуя вникания... :)
Сразу оговорюсь - основу здесь заложил Лавров сказанным в этой выдержке. Если смотреть завершающий п. 1.7.7 Гл. 1 - то он и проводит аналогию с непрерывным матаном. Указывая, что как там интегралы не от любых реальных "описаний явлений" берутся вообще или практически целесобразно в символьном виде (аналитически) - так и здесь не каждое алгоритмическое описание можно "взять в символах", алгоритмически же проанализировав его текст вкупе с исходными данными. И как непрерывные описания в этом случае нужно решать численно, с подстановкой данных в соответственно преобразованную матмодель - так и алгоописания бывает нужно исполнять, чтобы установить их свойства (соответствие требованиям).
    Но. Это, как и в обычном матане, отнюдь не отрицает формального подхода. Ибо в случаях, когда возможность аналитического решения неясна, надо сначала применить формальный анализ, чтобы это выяснить. Хотя бы анализ вида уравнения, чтобы выяснить - "берущееся" оно или нет...
И общий вывод Лаврова о том же - разработчик-аналитик формально строит семантику программы и так выявляет её определённость и соответствие семантике задачи (из формальной же спецификации). Где не получается - там предполагается необходимость прогона как эквивалента "численного решения". Но только там... и также опыт таких решений д.б. базой вывода новых формальных утверждений для символьного анализа...

У воопроса есть и другая сторона - понятия анализа нужно объяснить при изучении. И тут возможны разные пути - как и формы и методы выполнения. Для матана тот же Шур наглядно объясняет - есть базис элементарных функций, для которых нужно определить вид производных/интегралов. Типа как конструкции структурного программирования... или базисные ФАЛ. И есть любые другие функции - которые нужно представлять в базисе, чтобы матанализировать по схеме представления по-прежнему символьно. А не пытаться сразу вычислять. И тут возможна не чисто текстовая запись (Шур даёт для определения вида геометрическую интерпретацию, а для представления в базисе видов - графовую) - однако она есть изоморфизм к текстовой. И отнюдь не для поддержки "интуитивных" решений... :)

А с чем можно сравнить "альтернативный" подход? Я бы так сказал - с тем, когда разработчик правилами символьного анализа не пользуется, а любое уравнение сразу начинает решать численно. Ну можно в конечных разностях - а можно и на миллиметровке кривые строить... :) Так и здесь - можно всегда на отладчик полагаться, а можно на "мозговую проверку" описания как чисто внешнюю, без анализа свойств...

Не знаю, насколько получилось...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Роль цикла Дейкстры
СообщениеДобавлено: Среда, 06 Июнь, 2012 08:16 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
В связи с этим ещё некоторые соображения уже конкретно по ЦД. Сформировались на этом примере. Там видно, что преобразование структурной же конструкции "гнездо циклов" в ЦД делает структуру процесса, IMHO, более стройной. И даже сразу даёт некоторую оптимизацию.
Но есть ещё вещь, о которой там не писал. Дело в том, что ЦД данной задачи можно сам по себе эквивалентно преобразовывать. Меняя число веток и их структуру. И получалось так - можно повышать долю веток с линеаризованными телами, при этом число веток растёт.
И тут видится связь с непрерывным матаном снова. Можно сказать, что происходит "предельный переход". К чему? Очевидно, к сказанному здесь:
http://oberoncore.ru/wiki/структурирование_промышленного_цикла писал(а):
Основной смысл цикла — это его цель, в какое конечное состояние он должен привести (какое постусловие обеспечить). В состояние из каких возможных классов (например, у поиска два или более исхода: не нашли, нашли А, нашли Б… И т.п.) Действия же, которые в цикле происходят — это отнюдь не его смысл, а «грязная работа» по продвижению от начального состояния к целевому. Чем проще эти внутренние действия, тем лучше. И уж конечно, они не должны содержать вперемешку ещё и принятие решений о том, достигнута цель или нет.
Т.е. решение как бы "представляется рядами". Причём сложностью (маршрутной) членов ряда в случае ЦД можно управлять, "последовательно приближаясь" к предельному упрощению. Используя каждый раз формальное представление о задаче. Разумеется, для практики это когда целесообразно, а когда и не очень. Также нужно допускать, что иногда предел (полная линеаризация тел) достижим, иногда нет.
И получается, что сравнение доказательного программирования с матаном применительно к ЦД не только метафора. Можно сказать, что представление в виде ЦД - это и есть метод матанализа алгоритмов.
Уж не знаю, насколько правомерны такие рассуждения... :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Среда, 06 Июнь, 2012 22:21 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Такое впечатление, что народ глубоко задумался про инвариант цикла :)

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

Слишком простой пример, короче.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Четверг, 07 Июнь, 2012 06:12 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 710
Откуда: Псков
Для циклов поиска, наверное самый естественный инвариант - это отсутствие "искаемого" в текущем просмотренном:)
PS.
Под "просмотренным" понимается "до текущей точки(исключительно)"


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Четверг, 07 Июнь, 2012 13:12 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
albobin писал(а):
Для циклов поиска, наверное самый естественный инвариант - это отсутствие "искаемого" в текущем просмотренном:)
Да, но не оно главное.

----
Еще пунктик, которого не понимают недостаточно опытные в формальных методах люди вроде P.A. -- это что формальные методы никогда за пределами учебных работ (или автоматических систем) полностью формально не применяются, потому что это совершенно не нужный геморрой.

Важно уметь доводить до любой степени формализации в случае необходимости (если нужно уточнить, что-то проверить и т.п.).

В данном случае (как и в пресловутом разделе 1.9, если делать в реале, а не для учебника) инвариант настолько тривиален (предлагаю всё-таки его кому-нибудь выписать), что для доказательства корректности достаточно конъюнкции отрицаний бла-бла-бла.
Как бы ни серчал Peter Almazov насчет инварианта, эта самая конъюнкция выполняется в конце цикла и дает искомое постусловие.
В данном случае больше ничего и не нужно.

---
По поводу непонятности.
Ясное дело, надо знать, что откуда растет и куда смотреть (и что LOOP IF ... это стандартная в КП реализация ЦД).

Человек, полностью сделавший с карандашиком пяток упражнений на ЦД, сразу видит, что первый фактор (i<LEN) выйдет за скобки (как всегда в таких случаях), и остается нечто с двумя вторыми факторами.
Карандашиком чирк-чирк (если в уме не могём) -- и дело в шляпе.
Вот и весь формализьм.

Короче, учим матчасть, решаем пять задачек на ЦД.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Четверг, 07 Июнь, 2012 14:01 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 710
Откуда: Псков
Ну в данном случае инвариант сидит в oneZero.
В постусловии имеем по сути oneZero and oneZero, которые соотносятся к двум соседним элементам. То есть twoZero :)
PS.
истинность oneZero=(a[i]=0)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Четверг, 07 Июнь, 2012 20:27 

Зарегистрирован: Среда, 04 Июль, 2007 16:43
Сообщения: 247
Info21 писал(а):
В данном случае ... инвариант настолько тривиален

i <= LEN(a) :evil:


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 12 Июнь, 2012 07:03 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Info21 писал(а):
...формальные методы никогда за пределами учебных работ (или автоматических систем) полностью формально не применяются, потому что это совершенно не нужный геморрой.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 12 Июнь, 2012 12:57 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Владислав Жаринов писал(а):
Т.е. имеется в виду, что, если условия выбора (в т.ч. и в цикле) для формализации необходимы, то утверждения вроде инвариантов - необязательны? Но что не значает, что эти условия не нужно выводить?..
Что-то я не разобрался в этих двух предложениях. Но складывается впечатление, что Вы говорите о формализации цикла, а не формализации вообще. Но даже если ограничиться программированием и даже циклами, то можно сказать, что очень часто необходимые утверждения можно задавать не в формальном виде. При разумном использовании таких утверждений можно упростить рассуждения и существенно снизить вероятность ошибки в них. Но если ощущается, что неформальное утверждение не в должной степени строгое, то придётся пользоваться формализмами ("доводить до любой степени формализации в случае необходимости").


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 12 Июнь, 2012 19:40 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Да, в данном случае об инварианте цикла. Но сказанное, как я понял разных авторов, относится к математизации семантики любых программных конструкций.
Как я понял, отсюда и должно вытекать практическое ограничение, озвученное Info21 - повседневно рассуждаем только об "исполняемой логике" (условия ветвлений/циклов, ассерты, когда они ставятся) - а в целом доказываем правильность только если надо именно "проверять и уточнять".


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Пара примеров на цикл Дейкстры
СообщениеДобавлено: Вторник, 12 Июнь, 2012 21:12 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 710
Откуда: Псков
Не густо как то с предложениями инвариантов в тривиальном случае.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 55 ]  На страницу Пред.  1, 2, 3  След.

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 4


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2024, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB