Ich versteh nicht ganz, warum die Regel auf diese Art definiert wird.

—————-
{p/v->e}v:=e{p}.

Eigentlich müßte doch auch gelten:

—————-
{p}v:=e{p/e->v}.

Scheint mir von der Reihenfojge her logischer zu sein. Immerhin ist die Reihenfolge ja von der Vorbedingung zur Nachdebingung, die "Rechnung" läuft aber genau anders herum.

Beispiel:
zu beweisen: {y > 2} x = y+3 {x > 5}

der normale Weg ist ganz einfach,
man beginnt mit x = y+3 {x > 5} und kann dann durch diese Regel leicht auf die Vorbedingung {y+3 > 5}, also {y > 2} schließen

———

andersrum würde man von {y > 2} x = y+3 ausgehen
und wie willst du nun y+3 durch x ersetzen? y+3 steht ja gar nicht in der Vorbedingung,
da müsste man mühsam tricksen a la {y > 2} = {y+3 > 5} -> {x > 5} um die Nachbedingung auszurechnen,

—–

dass Problem ist also dass es immer sehr einfach ist eine Variable durch einen Ausdruck zu ersetzen, aber andersrum ein Ausdruck, der durch eine Variable ersetzt werden soll, in der Vorbedingung gar nicht so vorhanden sein muss..

dadurch hilft die Regel kaum weiter, man muss einen entscheidenen Schritt per Hand machen, ein Computer käme damit wohl weit weniger zurecht,

Ah, ok! Danke!