Hoare-Tripel für Zuordnung P{x/E} x:=E {P}

Question

Ich versuche, die bei Wikipedia vorgestellte Hoare-Logik zu verstehen.Hoare-Logik bei WikipediaAnscheinend bedeutet, wenn ich das richtig verstehe, ein Hoare-Tripel $$\{P\}~ C ~\{Q\}$$

Wenn P kurz vor C liegt, gilt Q unmittelbar nach C, solange C endet.(A)

Allerdings scheint das Zuordnungsaxiomschema anders interpretiert zu werden:

$$\frac{}{\{P[x/E]\} ~~x:=E~~ \{P\}}$$

Die Wikipedia sagt:

Das Zuweisungsaxiom bedeutet, dass die Wahrheit von $\{P[x/E]\}$ äquivalent zur Nachzuweisungswahrheit von $\{P\}$ ist.Wäre also nach dem Zuweisungsaxiom $\{P[x/E]\}$ vor der Zuweisung wahr, dann wäre $\{P\}$ danach wahr.Umgekehrt: Wäre $\{P[x/E]\}$ vor der Zuweisungsanweisung falsch, muss $\{P\}$ folglich falsch sein.

Ich denke, das Hoare-Triple bestätigt nur, dass, wenn P[x/E] vor x:=E, dann P(x) nach x:=E gilt.Es bestätigt per Definition NICHT, dass, wenn P(x) nach x:=E gilt, dann P[x/E] vor x:=E gilt.

Meine naive Frage ist: Wie kann $\{P[x/E]\}$ vor der Zuweisung äquivalent zu $\{P\}$ nach der Zuweisung sein?Steht dies im Widerspruch zu Punkt (A) am Anfang meines Beitrags?

Answer 1

Beachten Sie, dass Wikipedia genau das sagt

Das Zuweisungsaxiom bedeutet, dass die Wahrheit von $\{P[x/E]\}$ äquivalent zu ist Wahrheit nach der Zuweisung von $\{P\}$.

Mit anderen Worten: ($P$ gilt nach der Ausführung von $x:= E$), wenn ($P[x/E]$ gilt vor der Ausführung).Dies entspricht der von Ihnen bereitgestellten Definition $A$, die im Allgemeinen eine intuitivere Definition für das Hoare-Triple ist.

Answer 2

Es scheint, dass der Wortlaut des Wikipedia-Textes in gewisser Weise unzuverlässig ist:

Das Zuweisungsaxiom bedeutet, dass die Wahrheit von {P[x/E]} ist Äquivalent zur Nachzuweisungswahrheit von {P}.

Das Zuweisungsaxiom bedeutet das nicht.Es bedeutet nur, dass die Wahrheit von {P[x/E]} impliziert die Nachzuweisungswahrheit von {P}.Damit ist nicht die „Äquivalenz“ gemeint.

Allerdings ist die Gleichwertigkeit auch eine gültige Tatsache.Es ist nur so, dass das Hoare-Axiom für die Zuweisung es nicht sagt.

Eine gute Quelle für eine klare und strenge Behandlung von Hoare-ähnlichen Beweissystemen ist Apt und Olderog Überprüfung sequentieller und gleichzeitiger Programme.

Answer 3

Es bedeutet eher so etwas wie

Wenn P vor C wahr war, ist Q danach wahr.

Es gibt Zeitüberlegungen, da C normalerweise die Umgebung verändert.

Denken Sie an dieses Beispiel:$C=(x := 42)$ und $P=(x > 10)$.Dann macht die Instanz Ihrer Regel Sinn.

BEARBEITEN:Zeitüberlegungen sind wichtig.Hier $P$ mit „$x=E$“ (d. h.nachher) ist äquivalent zu $P[x/E]$ (vorher).Beachten Sie, dass „$x=E$“ nur das „Danach“ bezeichnet:es handelt sich nicht um eine echte Gleichheit, da $x$ in $E$ vorkommen kann.

Zum Beispiel

$$ {0 +42> 10 } ~~ x: = 0 ~~ {x +42> 10 } $$ $$ {x +42> 10 } ~~ x: = x +42 ~ ~ {x> 10 } $$

kann Ihnen helfen, das zu beweisen

$$ \{ \mbox{true} \} ~~ x:=0 ~;~ x := x + 42 ~~ \{ x>10 \}$$

Nebenbei bemerkt fand ich persönlich die Notation $P[x/E]$ sehr verwirrend.