Hoare Logic の演習について推論しています。
の評価ではストアを変更できないが、 の実行によってストアが変更され、 の値が変更される可能性があると仮定して、トリプル を満たすすべてのブール式BとすべてのプログラムSおよびを見つける必要があります。P{true} if B then S; if B then P; {a >= 0}BSB
a特に、事後条件にのみ存在し、このような例を見つけたことがないため、について何が言えるかわかりません。
ご協力いただきありがとうございます！
（私の以前の回答は間違っていました。）
トリプルを満たす式 ( B) とプログラム (Sおよび)は無数にあるため、問題は一種の制限のないものです。Pまた、トリプルは、タスクを単純な一般的な答えに減らすことができないほど複雑です。
基本的には、次のように分解できます。
Bが falseであるすべての状態について、a >= 0保持する必要があります (そうでない場合、トリプルは全体として保持できません)。Bが である州についてtrue、プログラムは次のS; if B then Pことを保証する必要があります。a >= 0Sの に当てはまり、BそのPような...
Sするか、Ba >= 0SなりB、...、等