OberonCore
https://forum.oberoncore.ru/

Еще раз о выходе из середины цикла
https://forum.oberoncore.ru/viewtopic.php?f=82&t=1500		 Страница 4 из 7
Автор:  Info21 [ Понедельник, 04 Май, 2009 21:58 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
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 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Info21 писал(а):
Или я ошибся в вычислении?
При (cmd = stop) обе ветки цикла имеют ложное условие, так что цикл завершится независимо от значения error.
Автор:  Александр Ильин [ Понедельник, 04 Май, 2009 22:36 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Код:
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:42 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Peter Almazov писал(а):
Ткните пальцем, наконец.
WHILE (cmd # empty) ... DO ... cmd := empty

Александр Ильин писал(а):
Постусловие:
Ни чего себе...
Автор:  Александр Ильин [ Понедельник, 04 Май, 2009 22:54 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Info21 писал(а):
(error # no_error) & ((cmd = empty) OR (cmd = stop))
Получается, что логические операции инвертированы (& вместо OR, и наоборот).
Поправка: что-то глупость я сморозил в 3 утра. Тут просто скобки вокруг OR надо убрать, и будет правильно.
Автор:  Александр Ильин [ Понедельник, 04 Май, 2009 23:03 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Александр Ильин писал(а):
Постусловие:
...
(cmd = stop) OR (cmd = empty) & (error # no_error)
Выходит, что цикл не завершится, пока не будет команды stop или empty, даже если уже есть error. Впрочем, empty выставляется сразу же после получения очередного значения error (после вызова Execute), так что проблемы в реализации тут нет.
Автор:  Илья Ермаков [ Понедельник, 04 Май, 2009 23:09 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
А error по инварианту может стать определённым только тогда, когда cmd = empty. Т.к. определён либо cmd, подлежащий выполнению, либо error от последнего выполнения.

Вообще, с циклом Дейкстры встаёт вопрос: должна ли реализация быть недетерминированной, как у него и предполагается? Не будет ли детерминированность способствовать непрозрачности цикла? Т.е. надо ещё учитывать порядок и неявные допущения, которые перекинуты из логических выражений на этот порядок..
Автор:  Valery Solovey [ Понедельник, 04 Май, 2009 23:14 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Info21 писал(а):
А случай stop без error как?
Так и надо по смыслу?
Это цикл Ильи. Я его просто переформатировал.
Автор:  Valery Solovey [ Понедельник, 04 Май, 2009 23:16 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Сергей Губанов писал(а):
Ни чего себе...
unchevosible
Автор:  Валерий Лаптев [ Вторник, 05 Май, 2009 07:50 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Илья Ермаков писал(а):
А error по инварианту может стать определённым только тогда, когда cmd = empty. Т.к. определён либо cmd, подлежащий выполнению, либо error от последнего выполнения.

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

1. Совершенно верно. Либо error от предыдущей - тогда надо заканчивать цикл. Либо error отсутствует, тогда есть следующая команда для выполнения.
2. Ну, поскольку цикл Дейкстры - это конечный автомат, то может, применить преобразование недетерминированного автомата в детерминированный?
Автор:  Peter Almazov [ Вторник, 05 Май, 2009 08:40 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Сергей Губанов писал(а):
Peter Almazov писал(а):
Ткните пальцем, наконец.
WHILE (cmd # empty) ... DO ... cmd := empty
Ну так этот кусок выполняется не один раз. В другой ветке GetCommand установит опять cmd # empty и т.д.

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

Т.н. "схема линейного поиска", выделенная для помощи тупым студентам, играет здесь отрицательную роль. Вместо того, чтобы внимательно изучить задачу, и честно определить инвариант, вспоминают про линейный поиск, а далее как в фильме 12 стульев: "Geben Sie mir bitte... - Ну это я знаю".
Автор:  Peter Almazov [ Вторник, 05 Май, 2009 08:46 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Александр Ильин писал(а):
Постусловие:
...длинный вывод пропущен...
Великолепно! Наглядная агитация: никогда не используйте этот идиотский вариант цикла, запотеете потом искать отрицание охран. Да и код часто придется дублировать.
Автор:  Пётр Кушнир [ Вторник, 05 Май, 2009 09:15 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Peter Almazov,
Ваша резкость не делает вам чести. Читать неприятно. Ну и всякие вердикты можно и обосновать, для тех, кому не очевидна их правильность.
А насчёт инварианта - как мне показалось, тут все только и говорят о том, что он необходим, поэтому ваши слова кажутся немного странными.
Автор:  Peter Almazov [ Вторник, 05 Май, 2009 09:45 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Пётр Кушнир писал(а):
Peter AlmazovА насчёт инварианта - как мне показалось, тут все только и говорят о том, что он необходим, поэтому ваши слова кажутся немного странными.
Это Вам правильно показалось, только вот ни один участник обсуждения его сформулировал. Кроме, нескромно замечу, меня.
Так что, чем упрекать в резкости, лучше бы привести инвариант.
Автор:  Valery Solovey [ Вторник, 05 Май, 2009 10:40 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Что-то я не видел Вашего инварианта.
Автор:  Peter Almazov [ Вторник, 05 Май, 2009 12:43 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Так на первой странице:
Peter Almazov писал(а):
Всё дело в том, что никто не сформулировал инвариант цикла. В моём решении он такой (неформально, естественно): есть указатель на команду, который задан переменными RA и first. Инвариант: команды от начала последовательности до указателя выполнены.
Автор:  Valery Solovey [ Вторник, 05 Май, 2009 12:54 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Возможно, для математической индукции это и инвариант, но что если часть этих команд не выполнено?
Автор:  Александр Ильин [ Вторник, 05 Май, 2009 12:56 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Valery Solovey писал(а):
Возможно, для математической индукции это и инвариант, но что если часть этих команд не выполнено?
В смысле, в результате условного/безусловного "перепрыгивания" через несколько команд (jmp)?
Автор:  Peter Almazov [ Вторник, 05 Май, 2009 13:01 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Valery Solovey писал(а):
Возможно, для математической индукции это и инвариант, но что если часть этих команд не выполнено?
Я тоже не вполне понял вопрос. В это время про команду jump ещё не было речи.
Автор:  Info21 [ Вторник, 05 Май, 2009 13:12 ]
Заголовок сообщения:  Re: Еще раз о выходе из середины цикла
Александр Ильин писал(а):
... Впрочем, empty выставляется сразу же после получения очередного значения error (после вызова Execute), так что проблемы в реализации тут нет.
Но есть проблема логической грязи.
Страница 4 из 7 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/