OberonCore

Но и Вы не попали в яблочко.

Найдите одну маленькую ошибочку в своем кандидате -- и останетесь победителем

Не ради победительства, а любопытства ради
Наверное, если уж формально подходить, надо бы не i , а i-1 (истинность инварианта должна же сохраняться после окончания цикла). Тогда надо ещё "усилием мысли" значение (a[i]=0) для i<0 считать равным FALSE.

PS.
Но, если и это не в яблочко, то яблочко явно райское
PPS.
Если авторский вариант иной, то может быть стоит затаить, а вдруг какой "блестящий" стрелок найдётся и попадёт в самую точку

Да, поправка такая.

Только почему "формально". Реально.
Истинность до цикла как раз и устанавливается установкой oneZero перед циклом.

Вероятно, нужно не забывать, что инвариант должен выполняться после i := i + 1.

Да, слово неподходящее. Имел ввиду "соблюдая строгость" или "... точность"

Слово "строгость" двусмысленно, лучше остановиться на слове "точность".

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

Вообще, отношение к ЦД такое же, какое долгое время была у русскоязычных программёров к SWITCH-методу Шалыто. Сколько Абрамыча по форумам поливали, что "ничего там нет, это нахрен не нужно, это банально, это тупо, мы и так код пишем прекрасно без всяких автоматов" и проч.
Хотя совершенно очевидно, что это метод, который позволяет во многих ситуациях регуляризовать решение задачи. Как можно запрограммировать состояние объекта и его изменение через раздельные переменные (булевы признаки и проч.) - и всегда будут и случаи, и сторонники, когда это будет, вроде, нагляднее. С другой стороны, проводились сравнения для сложных задач, что программист, нахреначивший кучу логических признаков и их изменения в разных местах, допускал много ошибок и долго отлаживался, а программист, вводящий одну переменную состояния и анализировавший регулярным образом все случаи, успешно решал задачу.

Так и ЦД позволяет по-другому подойти к построению алгоритма, вытащив на один уровень то, что расслоено обычно по нескольким. Иметь в арсенале такую штуку очень полезно.

При всей полезности, никто не имеет. В интернете нет ссылок, кроме как на здешнюю публику. Наберите запрос "применение цикла Дейкстры".

Психология барана в стаде.

Федор Василевич, как Вы предлагаете изучать вопрос статистики перехода программистами от теоретической идеи ЦД к практике применения?

Ну, для начала при таком употреблении понятия статистики можно вспомнить известное высказывание лорда Дизраэли о трёх видах лжи...

Если серьёзно - то переход уже состоялся. Т.к. у "автоматчиков" фактически и предлагается эмуляция ЦД по образцу, предложенному Фёдором Васильевичем для КомПаса. См. тех же Поликарпову и Шалыто - уже говорил. Возможно, изначально они "говорили прозой, не зная об этом" - но это лишь подтверждает практическую полезность этой конструкции, раз "от жизни" к ней приходят...
То же справедливо и для Дмитрия_ВБ, который ввёл как "цикл-силуэт" ту же эмуляцию... и тоже от практики, очевидно...

Федор Васильевич, какой запрос Вы используете или предлагаете для изучения в Интернете популярности ЦД у программистов?

Можете объявить конкурс на лучший запрос.

Ну, чтобы победить в таком конкурсе, прежде всего нужны данные, содержащиеся здесь и здесь (п/р 2.3)...
Имеется в виду, что искать надо в настоящее время в первую очередь различные формы эмуляции ЦД, применяемые при реализации и/или спецификации программ. И также смотреть - каким образом к ним пришли.

Владислав Жаринов, Вы не торопитесь, дождемся соображений Федора Васильевича. Ведь именно его не устроил запрос "применение цикла Дейкстры" в Интернете.

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

Федор Васильевич, Вы вероятно и сами желаете оценить результативность пропаганды теоретической идеи ЦД?

У меня в тексте сообщения(ий) используется термин "теоретическая идея ЦД", возможно ему синонимом будет термин "формальная идея ЦД"?

Подождём, разумеется... просто, если конкурс будет таки объявлен - то нелишне заранее подумать о возможных путях к победе...

Кстати, уже простой запрос "цикл Дейкстры" выдаёт результат ненулевой и физически (в смысле числа результатов поиска), и логически - в том смысле, что они образуют ещё ряд направлений, помимо того, что можно отнести к результатам пропаганды Фёдором Васильевичем... Ну там понятно, что одно из них - это рассмотрение в Драконографике и в ГРАФИТ-базисе - а среди иных самостоятельных прежде всего "Основания программирования" (неоднократно цитируемые на разных ресурсах), а также позиция Каймина (кстати, любопытно видеть её по "Лексикону программирования" или на Педсовете)... На нескольких форумах кто обсуждает ЦД, а кто и переписывает код в такой форме.

В общем, кому надо (для дела в том числе) - тот знает... так можно перефразировать замечание...

Меня этот вопрос не интересует.