Warum ist das Existentielle in den stärksten Nachbedingungen notwendig?

Question

Jede Formulierung des stärksten Nachbedingung Prädikat Transformators ich gesehen habe, stellt die Zuordnungsregel wie folgt:

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

Ich frage mich, warum ist die existentielle (und damit die existenzquantifizierte Variable „v“) notwendig, in den obigen Regel? Es scheint mir der stärkste Nachbedingungen Prädikat Transformator ist fast identisch mit symbolischen Bewertung, in dem Sie einen Zustand (eine Zuordnung von Variablen zu Werten) und eine Pfadbedingung (ein Prädikat, das an einem bestimmten Punkt im Programm muss wahr sein). Die symbolische Bewertung beruht jedoch nicht auf einem existenziellen Quantor.

Also, ich denke, ich muss hier etwas fehlen. Jede Hilfe wird geschätzt!

Answer 1

werde ich einige intuitive Beschreibung geben, da man einige Kenntnisse in symbolischer Auswertung hat

Wenn Sie eine beliebige Karte auf Variablen haben, können Sie nichts über zukünftige Zustandsänderungen in dem Programm sagen, bevor bei ihnen während der Suche Analyse.

Die symbolische Auswertung merkt sich jeden gewählten Pfad [als Zustandsraumtrennung], so dass er nicht in der zu lösenden Bewertungsformel enthalten sein muss.

Hier streiten Sie jedoch über jeden möglichen Pfad und benötigen daher eine beliebige Formel, um das Verhalten zu beschreiben.

Angenommen, Sie würden die Variable in der Formel behalten, dann würden Sie über nur 1 Pfad der möglichen Läufe streiten. Wenn Sie wissen, dass Ihre Variable keine anderen Pfade induziert, können Sie dieses Verhalten vereinfachen.

Haben Sie jedoch die schwächste liberale Vorbedingung, wissen Sie, von welchem ​​möglichen Pfad Sie beginnen und alle Pfade zusammenführen, um Eigenschaften über Ihr System zu prüfen.