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