なぜ事後的に最も強力な事後条件が必要ですか？次のように

Question

私が見てきた最強事後条件述語トランスのすべての製剤は、割り当てルールを提示：私は疑問に思って

sp(X:=E, P) = ∃v. (X=E[v/X] ∧ P[v/X]) 

、理由は実存（したがって、存在量化変数「V」）上記で必要ルール？最強の事後条件述語変換は、状態（変数から値へのマッピング）とパス条件（プログラムの特定の点で真でなければならない述語）を維持する点で、記号評価とほぼ同じです。しかし、象徴的な評価は、存在量限定子に依存していない。

私はここで何かを逃しているに違いないと思います。どんな助けもありがとう！

私は、いくつかの直感的な説明を与えるあなたはシンボリックな評価である程度の知識を持っているので、あなたが変数に任意のマップを持っている場合は、あなたが中にそれらを見て前に、プログラムで将来の状態の変化については何も言うことができない

Answer 1

分析。

記号評価は、選択された各パスを状態空間の分離として記憶しているため、解決する評価式に含まれる必要はありません。

しかし、ここではすべての可能な経路について主張し、したがって行動を説明するための任意の数式が必要です。

変数を数式に保持すると仮定した場合、実行可能な実行のパスは1つだけと主張します。変数が他のパスを誘導しないことが分かっている場合は、この動作を単純化できます。

しかしながら、最も弱い自由な前提条件がありますが、可能なパスからすべてのパスをまとめてラップし、システムに関するプルーフプロパティを確認してください。