1

我正在阅读“带有应用程序的语义 - 正式介绍”一书 - http://www.cs.ru.nl/~herman/onderwijs/semantics2019/wiley.pdf并对此有一些疑问：

  1. 在 Ex.2.22, p.39 中，要求表明表 2.2 的结构操作语义是确定性的。是否需要对推导树的形状进行归纳证明，类似于自然语义的证明方式，还是直接按照表2.2中每个规则的定义，证明是确实是确定性的？
  2. 在 Ex.6.24, p.190 中，要求显示在 While 语言中添加重复可保持系统完整。我将 [repeat] 的规则定义如下： [repeat]

通过这一点，我希望证明它持有 Q^¬B⇒P（其中 P= wlp（重复 S 直到 b，Q）），并从 [cons] 规则中获得 {P}S{Q} 部分通过证明 wlp(repeat S until b,Q) ⇒wlp(S,Q )，类似于书中证明 [while] 规则在 p.189 中完成的方式。出于某种原因，上述建议似乎对我不起作用。我对 [repeat] 规则的定义是否正确？如果是这样 - 我建议的证明方法是正确的还是我应该尝试不同的方法？

4

0 回答 0