OberonCore

На Королевстве Дельфи возникла тема о доказательном построении алгоритма вычисления исправленной дисперсии выборки.

Это послужило толчком к написанию следующей статейки:

Пример доказательного построения процедуры: вычисление несмещённой (исправленной) дисперсии.



Исходник в odc (Юникод):



Замечания, конечно, приветствуются.

1. У Гриса [3] нет "базовой схемы "полный проход"".
2. Это не "полный проход", а Ваш любимый линейный поиск (линейный просмотр, в терминах Дейкстры, [2], с. 146). Ищется первое НЕ real.
3. Тема не очень удачная. Внутренность цикла имеет вид x:=F(x). Такие примеры обычно решаются при изучении индуктивных функций (Кушниренко, [7]). А здесь индуктивные функции даже не упоминаются.

По поводу [3] - ошибка в ссылке, конечно.

Линейный поиск подразумевает дизъюнкцию в условии окончания (конъюнкцию в условии продолжения).
Это - полный проход (условие окончания - больше нет вещественных чисел).

Можно строить более "глубоко", но вопрос в целесообразности. Доказать правильность = представить в такой форме, чтобы правильность была очевидна.

Вообще-то такой вид - x := F(x, ...) - имеет внутренность любого цикла, манипулирующего переменными (x - вектор). В частном случае F не зависит от x, либо зависит только от x.

Конечно, при объяснении темы "Расчёт рекуррентных последовательностей" всё проговаривается подробнее, чем я сделал тут. Здесь принято, что человек умеет отображать рекуррентное выражение функции в тело цикла. Тем более, что функция, считаемая циклом, тривиальна - сумма.

Вообще, Пётр, Ваша "война" против базовых схем и подобных частных (но общих по статистике) случаев, мне совершенно непонятна. Они как раз и появились вследствие практического применения дисциплины программирования.

Понятно, что человек, владеющий общим аппаратом анализа, готов к решению любых задач оптимизации. Давайте на этом основании воевать против методов линейного программирования. И каждый раз в каждой задаче приходить к ним же. Сто раз к одному и тому же. Дисциплина программирования как раз должна устранять такое "велосипедостроение".

Не надо добавлять точки внутрь скобок, частный случай без точек - это и есть линейный просмотр. Прочтите внимательно Дейкстру. Там, правда, охрана зависит от x, но это несущественно.
Ещё раз повторяю, что этот пример больше подходит для объяснения индуктивных функций. Книги Кушниренко у меня под рукой нет, но можно посмотреть здесь http://www.intuit.ru/department/se/pbmsu/4/4.html и здесь http://www.intuit.ru/department/se/oip/tasks/6.html Задача 11.36

"Общий аппарат анализа" - методика, описанная Дейкстрой и Грисом не предполагает необходимости для решения задачи относить её к какой-либо базовой схеме. Это лишний шаг. Часто вредный.

На каком опыте это основано.

Что шаг лишний, видимо, нет возражений.
Основано на моём личном опыте.
Одно дело - распознать характер цикла и классифицировать его, это не вредно, а весьма полезно. Но это всё очень просто сделать, не надо переоценивать важность тривиальных вещей. В случае с полным проходом мозги после этого можно отключить. А в случае линейного поиска надо смотреть на условия задачи, а не на то, что это линейный поиск. Ибо шаблон один, а условия бывают весьма разные. В обсуждениях на форуме я часто наблюдаю обратный путь, что и считаю вредным. Но вести "войну", как выразился Илья, не собираюсь.
Вот если есть конкретные примеры, то их было бы интересно обсудить.

Есть, причем даже вступать в полемику, честно говоря, лень.

Аналогично

Линейный просмотр у Дейкстры - как раз и есть полный проход. Выраженный в общем виде.
Проход по последовательности неизвестной длинны от её начала до конца. Последовательность состоит из {x:~B(x)}.

Линейный поиск же подразумевает много причин окончания процесса - и классифицирует, так скажем, эти исходы.

P.S. При описании этих схем в терминах x := F(x) следует не забывать о случае управляющих алгоритмов, когда явно доступного алгоритму состояния может не быть вообще (т.е. идёт только выдача/получение сигналов/инструкций), а постусловие формулируется относительно цепи событий в системе. Не спорю, что и тут можно говорить о F(x), если трактовать x в нужном смысле (говорить о состоянии в смысле, специфичном для программируемой системы). Но всё же, отметим.

Очень интересное развитие темы вышло, в плане анализа погрешностей:
отсюда и далее -
http://delphikingdom.ru/asp/talktopic.a ... 95#msg4899

В итоге получился как раз успех доказательного подхода.

Надо статью дополнить, займусь завтра.

А, ну всё ясно, в терминах лекции 08 Вы совершенно правы. Я под этими терминами понимал другое, и пропустил эти рассуждения в лекции как очевидные. Как говориться, "...ну, это я знаю..."
Смотрел в книгу, а видел фигу.
Это возникло из-за того, что толкователи использовали те же термины, что и отцы-основатели, но абсолютно в другом смысле. Такой подлянки не ожидал просто. Определение Дейкстры я уже приводил, вот Гриса.
После таких фокусов какие бы то ни было обсуждения полностью теряют смысл.

А надо уточнять термины всегда, и вообще о смысле слов заботиться

Совет разумный. Можете применить его в лекции 08: "Если кто-нибудь знаком с работами Дейкстры и Гриса, забудьте про то, что они называют линейным поиском, и слушайте, что я так называю".

У меня непоняток не возникает.

А линейный поиск -- устоявшийся термин. (А Вы опять невнимательны.)

Кстати, по-поводу

формулы просто скопированные картинки или в среде BlackBox есть возможность генерить графическое представление формул изTeX-овского представления?

По виду формулы больше походят на MathType'овские (не TeX)

http://www.zinnamturm.eu/downloadsAC.htm#Casket.