我（错误地）学习了一门关于验证并发程序的课程，到目前为止，我们已经介绍了这种称为“Owicki-Gries 方法”的方法。显然，可以通过将断言与每个语句相关联来证明程序的各种结果，并表明这些断言是归纳的并且不会相互干扰。我们的一项任务涉及 Lamports 的快速互斥算法，详见本文：
在论文中，给出了互斥的 Owicki-Gries 风格证明。它看起来完全违反直觉。我很难理解的是如何首先提出这些断言？你什么时候知道这些断言既不是太强（太强以至于它破坏了干涉自由）也不是太弱（例如一些微不足道的东西，比如每个陈述的重言式）？
干杯
首先，为了了解 Owicki-Gries 方法，我强烈建议您查看本教科书中关于 Owicki-Gries 的两章。
（完整的教科书也可以在2021 年中期以草稿形式在这里找到，或者您可以通过电子邮件向摩根教授索取副本）
当您编写一个断言然后寻找证明局部正确性时，引用教科书“每个断言......都是紧接之前片段的后置条件，以及紧随其后的那个（代码行）的前置条件。
为了回答您的问题，您询问如何确定断言的强度。由于在每一行代码之前和之后都需要一个断言，因此断言的范围从极弱到中等弱。因此，我建议最初尝试一个适度弱的断言。
当您证明局部正确、全局不变量和全局正确性时，如果您意识到断言太强，您可以返回代码并削弱它们。相反，如果断言太弱，您可以尝试将它们调整得更强一些。
当它们支持您的程序运行同时满足 Owicki-Gries 的条件并满足安全性和活力的特性时，您知道它们是正确的力量。