OberonCore

А действительно, какой можно формальный инвариант записать для обычного цикла процессора?
Команды исполняются последовательно.
Если по одной команде в слове, то ничего не пропускается, останов только по error и стоп.
А вот если по две команде в слове, то если первая команда - переход, то вторую надо пропускать.
Как вообще инвариант-то записать? даже в первом варианте?

Не знаю. Инвариант не мой.

"команды от начала последовательности до указателя выполнены"

А если не выполнены? Что тогда?

Обратите внимание, что в моём решении цикл сделан не по словам, а по командам. Мы выполняем одну команду и продвигаем указатель на следующую. Инвариант остается истинным. Для jump-ов картина не сильно усложняется. Начало последовательности может меняться в процессе выполнения, но всегда выровнено на границу слова (first=true). Инвариант (неформально): выполнены все непрерывные последовательности команд, которые встретилсь от начального положения до каждого очередного jump и выполнены все команды в последовательности от последего jump (или старта) до текущего положения указателя.
Если делать цикл по словам, как это предлагали некоторые, то инвариант будет совершенно другой. Какой – пусть напишут авторы.

Народ! Хватит тупить! Нету здесь цикла Дейкстры. Здесь проще:

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

Изначально здесь классический цикл:


И не классическая процедура выбора:

Интересный подход!
Надо будет посмотреть...

Но сколько вариантов получилось - просто блеск!

И, что характерно, про инвариант опять ни слова

А чего переливать из пустого в порожнее? Там два действия. Они и есть инвариант.

P.S. Так что будет, если не все команды выполнены?

Да то же самое, что будет, если 2*2 = 5

Не все команды выполнены - так не бывает. Процеессор (в смысле интерпретатор) последовательно выбирает из памяти слова в регистр команд. Потом из регистра команд вытаскивает первую команду. Выполняет. Если нет ошибок, не стоп или не переход, то из регистра команд вытаскивается вторая команда. Если нет ошибок или не стоп, то новый шаг цикла. То есть на первой половине цикла - дополнительное условие - не переход.

Вторая часть инструкции не должна выполнятся если первая была jump.

RunCommand при выполнении jump меняет RA и выставляет first...

При чём тут тупые студенты? На практике эти две схемы - 90% по количеству от всех циклов.
Инвариант - это замечательно. Но полная его формальная запись нужна, когда есть варьируемые величины (т.е. цикл вычисляющего характера). А для такого рода достаточно чётко его проговорить, неформально. Формальнее некогда, да и не окупает себя для этого примера (доказательность # формальность).
Мой вариант не идеален, но я в этой ветке и не стремился давать эталонные примеры... Как вариант подхода сгодится.

viewtopic.php?p=28602#p28602 - приведён неформальный инвариант
viewtopic.php?p=28607#p28607
viewtopic.php?p=29047#p29047 - опираемся на него

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

Согласен. Обычный поиск. А цикл Ильи Евгеньевича все-таки неправильный

Действительно, слова про инвариант были, спасибо. Но у нас, оказывается, разный взгляд на инвариант. Ваш подход нужно будет осмыслить, это интересно.
Но в данном конкретном случае я совершенно не согласен. В конце концов, какой инвариант у линейного поиска? А такой: в просмотренной части массива не содержится искомый элемент. В совокупности с отрицанием охраны после цикла это даёт решение задачи. В этом посте viewtopic.php?p=28602#p28602 смешивается инвариант (сомнительный для меня) и охрана цикла. Даже чисто формально, это неверно.

С оценкой 90% согласен полностью. Но, насколько я помню, ни Дейкстра, ни Грис не рассматривали такой шаблон как "линейный поиск". Пример с поиском в 2-х мерном массиве - это просто один из примеров, ничем не выделяющийся среди остальных. А "линейный поиск" придумали толкователи, чтобы легче было объяснять [тупым студентам].
Я согласен, что в данном примере всё сводится к пресловутому линейному поиску. Но это мало чем может помочь, дьявол в деталях. Можно организовать цикл по словам, а можно и по полусловам, или как в Вашем варианте по полусловам "с мерцанием". Везде будет линейный поиск. Но это принципиально разные решения, инвариант будет совершенно разный. На взгляд человека, не врубающегося в тему, все они очень похожи. Но эта похожесть сродни похожести правильной программы, на программу, содержащую ошибки. Поэтому надо решать конкретную задачу, а не выискивать линейный поиск.

Что есть конкретная задача?
Конкретная задача - моделирование работы процессора:
На каждом шаге процессор выбирает и выполняет команду, пока не встретит команду остановки или неизвестную команду (ошибка)

получается тривиальный цикл.

Далее рассматриваем "детали":

Но тут выясняется, что в одном слове содержится две команды, поэтому и усложняется процедура.

Процедуру "исполнить_команду" особо рассматривать не стоит, так как внутри у неё классический конечный автомат со всеми вытекающими:

Да, я сразу и предложил такое решение.

А наворачивать потом стал с циклом Дейкстры из-за "щепетильности": ведь после выполнения команды может стать ясно, что следующую выбирать уже и не надо В данном случае - неважно, но могут быть случаи, где важно. (Сергей Губанов довольствуется просто IF-ом внутри, мне его вариант не нравится... Не люблю держать в цикле конструкции, которые срабатывают только 1 раз...)

> ... Не люблю ...

Вот и всё объяснение. Зато честно.