Я читал книгу "СЕМАНТИКА С ПРИЛОЖЕНИЯМИ - ФОРМАЛЬНОЕ ВВЕДЕНИЕ" - http://www.cs.ru.nl/~herman/onderwijs/semantics2019/wiley.pdf и у меня было несколько вопросов по этому поводу:
- В Ex.2.22, с.39 предлагается показать, что структурная операционная семантика таблицы 2.2 является детерминированной c. Требуется ли доказать это индукцией по форме дерева деривации, аналогично тому, как это доказано для случая естественной семантики, или это можно показать непосредственно, следуя определению каждого правила в таблице 2.2 и показывая, что оно действительно определено c?
- В Ис.6.24, стр.190, предлагается показать, что добавление повторения к языку Пока поддерживает систему завершенной. Я определил правило для [repeat] следующим образом: [repeat]
Этим я надеялся показать, что оно содержит Q ^ ¬B⇒P (где P = wlp (повторять S до b, Q)) и получить часть {P} S {Q} из правила [cons], показывая, что wlp (повторять S до b, Q) ⇒wlp (S, Q), аналогично Кстати, в книге доказано, что правило [while] завершено в p.189. По какой-то причине вышеприведенное предложение, похоже, не работает для меня. Правильно ли мое определение для правила [repeat]? Если так - мой предложенный способ доказать это правильно или я должен попробовать другой подход?