theorem-proving - 需要帮助理解 Owicki-Gries 方法

Question

我(错误地)学习了关于验证并发程序的类(class)，到目前为止我们已经介绍了这种称为“Owicki-Gries 方法”的方法。显然，可以通过将断言与每个语句相关联来证明有关程序的各种结果，并表明这些断言是归纳的并且不会相互干扰。我们的任务之一涉及 Lamports 的快速互斥算法，detailed in this paper :

在论文中，给出了互斥的 Owicki-Gries 式证明。它看起来完全反直觉。我很难理解的是，首先如何提出这些断言？你什么时候知道这些断言既不太强(强到破坏干扰自由)也不太弱(例如一些微不足道的东西，比如每个陈述的同义反复)？

干杯

Answer 1

首先，并提供对 Owicki-Gries 方法的理解，我强烈建议查看关于 Owicki-Gries 的两章，可以在 this 中找到。教科书。
(完整的教科书也可以在 2021 年年中以草稿格式 here 找到，或者您可以发送电子邮件 Professor Morgan 索取副本)
当你写一个断言然后试图证明局部正确性时，引用教科书“每个断言......都是
紧接之前的片段，以及紧接其后的(代码行)的先决条件。
要回答您的问题，您会询问如何确定断言的强度。由于在每一行代码之前和之后都需要一个断言，所以断言的范围从极弱到中等弱。因此，我建议最初尝试适度弱的断言。
当您证明局部正确、全局不变量和全局正确性时，如果您意识到断言太强，您可以返回代码并削弱它们。相反，如果断言太弱，您可以尝试将它们调整为更强一些。
当它们支持您的程序运行，同时满足 Owicki-Gries 的条件并满足安全性和活力的特性时，您就知道它们是正确的力量。