OberonCore

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

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




Начать новую тему Ответить на тему  [ Сообщений: 122 ]  На страницу Пред.  1, 2, 3, 4, 5, 6, 7  След.
Автор Сообщение
СообщениеДобавлено: Вторник, 05 Май, 2009 13:16 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3261
Откуда: Астрахань
А действительно, какой можно формальный инвариант записать для обычного цикла процессора?
Команды исполняются последовательно.
Если по одной команде в слове, то ничего не пропускается, останов только по error и стоп.
А вот если по две команде в слове, то если первая команда - переход, то вторую надо пропускать.
Как вообще инвариант-то записать? даже в первом варианте?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 13:18 

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 14:27 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 14:44 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
Валерий Лаптев писал(а):
Между прочим, в процессе отладки в цикле выяснился еще один нюанс.
Код:
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))


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 14:59 
Аватара пользователя

Зарегистрирован: Суббота, 12 Июль, 2008 22:49
Сообщения: 575
Откуда: Россия, Санкт-Петербург
Мне кажется, что столько споров исключительно из-за неправильного дизайна системы.

Изначально здесь классический цикл:
Код:
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 

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 15:15 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 563
Откуда: Москва
Валерий Лаптев писал(а):
Но сколько вариантов получилось - просто блеск!
И, что характерно, про инвариант опять ни слова :)


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 15:23 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
А чего переливать из пустого в порожнее? Там два действия. Они и есть инвариант.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 15:28 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 563
Откуда: Москва
Да то же самое, что будет, если 2*2 = 5


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 15:31 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3261
Откуда: Астрахань
Не все команды выполнены - так не бывает. Процеессор (в смысле интерпретатор) последовательно выбирает из памяти слова в регистр команд. Потом из регистра команд вытаскивает первую команду. Выполняет. Если нет ошибок, не стоп или не переход, то из регистра команд вытаскивается вторая команда. Если нет ошибок или не стоп, то новый шаг цикла. То есть на первой половине цикла - дополнительное условие - не переход.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 16:23 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
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 
Модератор
Аватара пользователя

Зарегистрирован: Среда, 16 Ноябрь, 2005 00:53
Сообщения: 4625
Откуда: Россия, Орёл
RunCommand при выполнении jump меняет RA и выставляет first...


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 17:36 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Peter Almazov писал(а):
Т.н. "схема линейного поиска", выделенная для помощи тупым студентам, играет здесь отрицательную роль.


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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 17:43 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Peter Almazov писал(а):
ни один участник обсуждения его сформулировал. Кроме, нескромно замечу, меня.
Так что, чем упрекать в резкости, лучше бы привести инвариант.

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 18:19 
Аватара пользователя

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 18:44 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 563
Откуда: Москва
Илья Ермаков писал(а):
http://forum.oberoncore.ru/viewtopic.php?p=28602#p28602 - приведён неформальный инвариант
viewtopic.php?p=28607#p28607
viewtopic.php?p=29047#p29047 - опираемся на него

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 19:12 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 22:10 
Аватара пользователя

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

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

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

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

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


Последний раз редактировалось Madzi Среда, 06 Май, 2009 17:51, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 05 Май, 2009 22:58 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Да, я сразу и предложил такое решение.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 06 Май, 2009 12:08 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
> ... Не люблю ...

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


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

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


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

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


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

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