OberonCore
https://forum.oberoncore.ru/

Еще раз о выходе из середины цикла
https://forum.oberoncore.ru/viewtopic.php?f=82&t=1500
Страница 5 из 7

Автор:  Валерий Лаптев [ Вторник, 05 Май, 2009 13:16 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Valery Solovey [ Вторник, 05 Май, 2009 13:18 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Александр Ильин писал(а):
Valery Solovey писал(а):
Возможно, для математической индукции это и инвариант, но что если часть этих команд не выполнено?
В смысле, в результате условного/безусловного "перепрыгивания" через несколько команд (jmp)?
Не знаю. Инвариант не мой.

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

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

Автор:  Peter Almazov [ Вторник, 05 Май, 2009 14:27 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Сергей Губанов [ Вторник, 05 Май, 2009 14:44 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Валерий Лаптев писал(а):
Между прочим, в процессе отладки в цикле выяснился еще один нюанс.
Код:
while (true)
{
    RM = mem[RA]; // выбрать слово
    RA = (RA + 1) % N; // изменение адреса - по модулю 1024
    RC = RM.cmd.first; // выбрать команду first
    run(); // выполнить команду
    if (Jump) continue; // если переход, то не выполнять вторую команду [/b]
    if (Error || stop) break; // если команда stop или ошибка
    RC = RM.cmd.second; // выбрать команду second
    run(); // выполнить команду
    if (Error || stop) break; // если команда stop или ошибка
}
Как это учесть в цикле Дейкстры, который Илья Ермаков написал?
Народ! Хватит тупить! Нету здесь цикла Дейкстры. Здесь проще:
Код:
do
{
   RM = mem[RA];
   RA = (RA + 1) % N;
   RC = RM.cmd.first;
   run();
   if (!(Jump || Error || stop))
   {
      RC = RM.cmd.second;
      run();
   }
}
while (!(Error || stop))

Автор:  Madzi [ Вторник, 05 Май, 2009 14:59 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Изначально здесь классический цикл:
Код:
cmd := GetCommand ();
WHILE cmd # cmdSTOP DO
    RunCommand (cmd);
    cmd := GetCommand ();
END;


И не классическая процедура выбора:
Код:
VAR
    mem : ARRAY OF ..
    first : BOOLEAN; (* TRUE *)
    RM, RA, RC: ...
PROCEDURE GetCommand (): BYTE;
BEGIN
    IF first THEN
        RM := mem[RA];
        RA := (RA + 1) MOD N;
        RC := RM MOD 256;
    ELSE
        RC := RM DIV 256;
    END;
    first := ~first;
END;

Автор:  Валерий Лаптев [ Вторник, 05 Май, 2009 15:08 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

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

Автор:  Peter Almazov [ Вторник, 05 Май, 2009 15:15 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Валерий Лаптев писал(а):
Но сколько вариантов получилось - просто блеск!
И, что характерно, про инвариант опять ни слова :)

Автор:  Valery Solovey [ Вторник, 05 Май, 2009 15:23 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

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

Автор:  Peter Almazov [ Вторник, 05 Май, 2009 15:28 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Валерий Лаптев [ Вторник, 05 Май, 2009 15:31 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Сергей Губанов [ Вторник, 05 Май, 2009 16:23 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Madzi писал(а):
Код:
PROCEDURE GetCommand (): BYTE;
BEGIN
    IF first THEN
        RM := mem[RA];
        RA := (RA + 1) MOD N;
        RC := RM MOD 256;
    ELSE
        RC := RM DIV 256;
    END;
    first := ~first;
END;
Вторая часть инструкции не должна выполнятся если первая была jump.

Автор:  Евгений Темиргалеев [ Вторник, 05 Май, 2009 16:27 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Илья Ермаков [ Вторник, 05 Май, 2009 17:36 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Peter Almazov писал(а):
Т.н. "схема линейного поиска", выделенная для помощи тупым студентам, играет здесь отрицательную роль.


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

Автор:  Илья Ермаков [ Вторник, 05 Май, 2009 17:43 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Peter Almazov писал(а):
ни один участник обсуждения его сформулировал. Кроме, нескромно замечу, меня.
Так что, чем упрекать в резкости, лучше бы привести инвариант.

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

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

Автор:  Info21 [ Вторник, 05 Май, 2009 18:19 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Peter Almazov [ Вторник, 05 Май, 2009 18:44 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Илья Ермаков писал(а):
http://forum.oberoncore.ru/viewtopic.php?p=28602#p28602 - приведён неформальный инвариант
viewtopic.php?p=28607#p28607
viewtopic.php?p=29047#p29047 - опираемся на него

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

Автор:  Peter Almazov [ Вторник, 05 Май, 2009 19:12 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

Автор:  Madzi [ Вторник, 05 Май, 2009 22:10 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

Что есть конкретная задача?
Конкретная задача - моделирование работы процессора:
На каждом шаге процессор выбирает и выполняет команду, пока не встретит команду остановки или неизвестную команду (ошибка)
Код:
команда := выбор_команды ();
ПОКА (команда # ОСТАНОВ) И (команда # ОШИБКА) ДЕЛАТЬ
    исполнить_команду (команда);
    команда := выбор_команды ();
ПОКАВСЕ;

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

Далее рассматриваем "детали":
Код:
ПРОЦЕДУРА выбор_команды (): команда;
НАЧАЛО
    команда := память[указатель_команд];
    указатель_команд := указатель_команд + 1;
ПРОЦЕДУРАВСЕ;

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

Процедуру "исполнить_команду" особо рассматривать не стоит, так как внутри у неё классический конечный автомат со всеми вытекающими:
Код:
ПРОЦЕДУРА исполнить_команду (команда);
НАЧАЛО
    ВЫБОР команда ИЗ
        ОСТАНОВ:...
        СЛОЖЕНИЕ:...
    ВЫБОРВСЕ;
ПРОЦЕДУРАВСЕ;

Автор:  Илья Ермаков [ Вторник, 05 Май, 2009 22:58 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

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

Автор:  Сергей Губанов [ Среда, 06 Май, 2009 12:08 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла

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

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

Страница 5 из 7 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/