Es geht um die Zuweisung bei Arrays in Kapitel 3, Teil 1, Seite 18.

Hier wird eine neue Schlussregel für Array Assignment eingeführt, bei der anstatt, nur der Wert , das Array substituiert wird.

Damit soll dann angeblich das Beispiel (Im Kasten) beweisbar sein:
{j=i AND j=z OR j!=i AND X(j)=z} X(i) := y {X(j)=z}

Warum brauchen wir die neue Regel genau (SP RULE: Partial Correctness for Array Assignment)? Und wie soll damit das Beispiel beweisbar sein? Wir würden sagen, das Beispiel ist mit der neuen Regel auch nicht zu beweisen.

Die Regeln braucht man um Vorbedingungen über den Index nutzen zu können.
Die herkömmliche Assignment-Rule erlaubt es ja nur, die ganze linke Seite einer
Zuweisung in der Vorbedingung zu ersetzen, während bei AAP Index und Array
getrennt behandelt werden.

Zur Abkürzung setze man zunächst [latex]P=((j=i \wedge y=z) \vee (j\ne i \wedge X(j)=z))[/latex].
Dann ist klar [latex]P\Rightarrow [X|i:y](j)=z[/latex]
und [latex]P\Rightarrow ((j=i\wedge y=z)\vee(j\ne i\wedge [X|i:y](j)=z))[/latex], also

[latex]P \Rightarrow ((j=i \wedge y=z)\vee(j\ne i\wedge [X|i:y](j)=z))\wedge [X|i:y](j)=z.[/latex] (*)
Wendet man auf [latex]p=((j=i \wedge y=z)\vee(j\ne i\wedge X(j)=z) \wedge X(j)=z)[/latex] die
Regel AAP an, so erhält man
[latex]\{ ((j=i \wedge y=z)\vee(j\ne i\wedge [X|i:y](j)=z)\wedge [X|i:y](j)=z \} X(i):=y \{((j=i\wedge y=z)\vee(j\ne i \wedge X(j)=z))\wedge X(j)=z \}.[/latex]
Läßt man nun SP mithilfe von (*) die Vorbedingung auf P bringen
und WC die Nachbedingung auf X(j)=z, ist die Spezifikation hergeleitet.

danke