私は (誤って) 並行プログラムの検証に関するコースを受講しており、これまで「Owicki-Gries 法」と呼ばれるこの方法について説明してきました。どうやら、アサーションを各ステートメントに関連付けることで、プログラムに関するさまざまな結果を証明し、これらのアサーションが帰納的であり、互いに干渉しないことを示すことができます。私たちの課題の 1 つは、Lamports の Fast Mutual Exclusion アルゴリズムに関するもので、この論文で詳しく説明しています。
この論文では、相互排除のための Owicki-Gries スタイルの証明が与えられています。それは完全に直感に反するように見えます。私が理解するのに苦労しているのは、そもそもこれらの主張をどのように考え出すかということですか? これらの主張が強すぎず (干渉の自由を壊すほど強い) も弱すぎもしない (たとえば、各ステートメントのトートロジーのような些細なこと) はいつわかりますか?
乾杯