OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Четверг, 14 Ноябрь, 2019 22:43

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




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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8196
Откуда: Троицк, Москва
Valery Solovey писал(а):
Каждая строка за исключением END - ветка

Код:
WHILE (cmd # empty) & (cmd # stop) DO Execute(cmd, error); cmd := empty
ELSIF (cmd = empty) & (error = no_error) DO GetCommand(cmd)
END
У меня странное постусловие выходит.
(error # no_error) & ((cmd = empty) OR (cmd = stop))
Т.е. на выходе обязательно есть error. А случай stop без error как?
Так и надо по смыслу?
Или я ошибся в вычислении?


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

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2316
Откуда: Россия, Томск
Info21 писал(а):
Или я ошибся в вычислении?
При (cmd = stop) обе ветки цикла имеют ложное условие, так что цикл завершится независимо от значения error.


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

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2316
Откуда: Россия, Томск
Код:
WHILE (cmd # empty) & (cmd # stop) DO Execute(cmd, error); cmd := empty
ELSIF (cmd = empty) & (error = no_error) DO GetCommand(cmd)
END

Постусловие:
~((cmd # empty) & (cmd # stop)) & ~((cmd = empty) & (error = no_error)) => (первое отрицание вносим в скобки)
((cmd = empty) OR (cmd = stop)) & ~((cmd = empty) & (error = no_error)) = (обозначим выражения буквами)
(A OR B) & ~(A & C) => (отрицание вносим в скобки)
(A OR B) & (~A OR ~C) => (приведём к ДНФ, "перемножив" скобки)
(A & ~A) OR (A & ~C) OR (B & ~A) OR (B & ~C) => (первый дизъюнкт всегда ложен - выбрасываем)
(A & ~C) OR (B & ~A) OR (B & ~C) => (подставляем вместо букв выражения)
(cmd = empty) & ~(error = no_error) OR (cmd = stop) & ~(cmd = empty) OR (cmd = stop) & ~(error = no_error) => (во втором дизъюнкте правую часть можно выбросить, так как она истинна всегда, когда истинна левая часть, т.е. не влияет на значение конъюнкции)
(cmd = empty) & ~(error = no_error) OR (cmd = stop) OR (cmd = stop) & ~(error = no_error) => (третий дизъюнкт тоже можно выбросить, так как он является ослабленным вариантом второго)
(cmd = empty) & ~(error = no_error) OR (cmd = stop) => (поменяем местами дизъюнкты, внесём отрицание в скобки)
(cmd = stop) OR (cmd = empty) & (error # no_error)


Последний раз редактировалось Александр Ильин Понедельник, 04 Май, 2009 22:51, всего редактировалось 4 раз(а).

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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
Peter Almazov писал(а):
Ткните пальцем, наконец.
WHILE (cmd # empty) ... DO ... cmd := empty

Александр Ильин писал(а):
Постусловие:
Ни чего себе...


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

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2316
Откуда: Россия, Томск
Info21 писал(а):
(error # no_error) & ((cmd = empty) OR (cmd = stop))
Получается, что логические операции инвертированы (& вместо OR, и наоборот).
Поправка: что-то глупость я сморозил в 3 утра. Тут просто скобки вокруг OR надо убрать, и будет правильно.


Последний раз редактировалось Александр Ильин Вторник, 05 Май, 2009 08:14, всего редактировалось 1 раз.

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

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2316
Откуда: Россия, Томск
Александр Ильин писал(а):
Постусловие:
...
(cmd = stop) OR (cmd = empty) & (error # no_error)
Выходит, что цикл не завершится, пока не будет команды stop или empty, даже если уже есть error. Впрочем, empty выставляется сразу же после получения очередного значения error (после вызова Execute), так что проблемы в реализации тут нет.


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

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9154
Откуда: Россия, Орёл
А error по инварианту может стать определённым только тогда, когда cmd = empty. Т.к. определён либо cmd, подлежащий выполнению, либо error от последнего выполнения.

Вообще, с циклом Дейкстры встаёт вопрос: должна ли реализация быть недетерминированной, как у него и предполагается? Не будет ли детерминированность способствовать непрозрачности цикла? Т.е. надо ещё учитывать порядок и неявные допущения, которые перекинуты из логических выражений на этот порядок..


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

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Info21 писал(а):
А случай stop без error как?
Так и надо по смыслу?
Это цикл Ильи. Я его просто переформатировал.


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

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Сергей Губанов писал(а):
Ни чего себе...
unchevosible


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

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3108
Откуда: Астрахань
Илья Ермаков писал(а):
А error по инварианту может стать определённым только тогда, когда cmd = empty. Т.к. определён либо cmd, подлежащий выполнению, либо error от последнего выполнения.

Вообще, с циклом Дейкстры встаёт вопрос: должна ли реализация быть недетерминированной, как у него и предполагается? Не будет ли детерминированность способствовать непрозрачности цикла? Т.е. надо ещё учитывать порядок и неявные допущения, которые перекинуты из логических выражений на этот порядок..

1. Совершенно верно. Либо error от предыдущей - тогда надо заканчивать цикл. Либо error отсутствует, тогда есть следующая команда для выполнения.
2. Ну, поскольку цикл Дейкстры - это конечный автомат, то может, применить преобразование недетерминированного автомата в детерминированный?


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

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 530
Откуда: Москва
Сергей Губанов писал(а):
Peter Almazov писал(а):
Ткните пальцем, наконец.
WHILE (cmd # empty) ... DO ... cmd := empty
Ну так этот кусок выполняется не один раз. В другой ветке GetCommand установит опять cmd # empty и т.д.

Вообще, я крайне скептически отношусь к этому коду Ильи. GetCommand не определена, хотя должна бы для такого простого примера; введено empty, которое взялось ниоткуда и в котором нет никакой необходимости; инвариант не определён. Всё это можно отнести к категории dirty hack.

Т.н. "схема линейного поиска", выделенная для помощи тупым студентам, играет здесь отрицательную роль. Вместо того, чтобы внимательно изучить задачу, и честно определить инвариант, вспоминают про линейный поиск, а далее как в фильме 12 стульев: "Geben Sie mir bitte... - Ну это я знаю".


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

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


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

Зарегистрирован: Вторник, 29 Август, 2006 12:32
Сообщения: 2625
Откуда: Россия, Ярославль
Peter Almazov,
Ваша резкость не делает вам чести. Читать неприятно. Ну и всякие вердикты можно и обосновать, для тех, кому не очевидна их правильность.
А насчёт инварианта - как мне показалось, тут все только и говорят о том, что он необходим, поэтому ваши слова кажутся немного странными.


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

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 530
Откуда: Москва
Пётр Кушнир писал(а):
Peter AlmazovА насчёт инварианта - как мне показалось, тут все только и говорят о том, что он необходим, поэтому ваши слова кажутся немного странными.
Это Вам правильно показалось, только вот ни один участник обсуждения его сформулировал. Кроме, нескромно замечу, меня.
Так что, чем упрекать в резкости, лучше бы привести инвариант.


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

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Что-то я не видел Вашего инварианта.


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

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 530
Откуда: Москва
Так на первой странице:
Peter Almazov писал(а):
Всё дело в том, что никто не сформулировал инвариант цикла. В моём решении он такой (неформально, естественно): есть указатель на команду, который задан переменными RA и first. Инвариант: команды от начала последовательности до указателя выполнены.


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

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


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

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2316
Откуда: Россия, Томск
Valery Solovey писал(а):
Возможно, для математической индукции это и инвариант, но что если часть этих команд не выполнено?
В смысле, в результате условного/безусловного "перепрыгивания" через несколько команд (jmp)?


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

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 530
Откуда: Москва
Valery Solovey писал(а):
Возможно, для математической индукции это и инвариант, но что если часть этих команд не выполнено?
Я тоже не вполне понял вопрос. В это время про команду jump ещё не было речи.


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

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8196
Откуда: Троицк, Москва
Александр Ильин писал(а):
... Впрочем, empty выставляется сразу же после получения очередного значения error (после вызова Execute), так что проблемы в реализации тут нет.
Но есть проблема логической грязи.


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

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


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

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


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

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