Vor/Nachbedingung und Schleifeninvariante
-
Wie kommt man auf nach folgendem Code auf die VOR und NACH Bedingung?
also warum ist Y>=0?
und warum ist Nachbedingung:
Z=X*Yworan erkennt man das?
-
BunterVogel schrieb:
also warum ist Y>=0?
Das „muss sein“ damit die Schleife terminiert.
und warum ist Nachbedingung:
Z=X*YDie Schleife wird Y-mal durchlaufen, jedesmal wird auf Z, was anfänglich 0 ist, X addiert => Z = X*Y
-
BunterVogel schrieb:
Wie kommt man auf nach folgendem Code auf die VOR und NACH Bedingung?
also warum ist Y>=0?
und warum ist Nachbedingung:
Z=X*Yworan erkennt man das?
Wäre Y < 0, würde die Schleife niemals abbrechen.
Und Z = X*Y, weil X Y-mal addiert wird (weil davor W = Y gesetzt wird).
-
danke, warum wird in der nachbedingung nur das sich verändernde Z betrachtet und nicht W? W wird ja auch um 1 kleiner jedes mal..
-
Weil W nicht zum Output gehört, d.h. es existiert nach dem Ausführen der Funktion gar nicht mehr.
-
BunterVogel schrieb:
danke, warum wird in der nachbedingung nur das sich verändernde Z betrachtet und nicht W? W wird ja auch um 1 kleiner jedes mal..
W ist für den Algorithmus (als Black Box) wurscht. Und mit jedem beliebigen X gehts auch immer. Deshalb interessieren sie nicht.
-
ok, hatte ich mir gedacht...
also die Vorbedingung ist y >= 0 weil die Schleife durchlaufen wird bis y = 0 wird. Dann bricht sie ab.
und Z = X * Y , weil X Y Mal addiert wird (halt bei jedem Schleifendurchgang)danke
-
Nun hat man noch eine Schleifeninvariante eingeführt:
P = ( X * Y = Z + W * X )
Wie kommt man nun darauf?
-
Ich habe z.B
Falls a>0 dann a=2
Sonst a=1;Wie wären hier die VOR und NACH Bedingungen.
{a Element aus R UND a > 0} HIER MUSS WAS HIN ?{a=2}
UND
{a Element aus R UND NICHT(a>0)} HIER MUSS WAS HIN? {a=1}Ich habe das analog zu folgender Mitschrift gemacht:
Bei Selektion:
{VOR} IF B THEN alpha ELSE beta FI {NACH}
daraus folg
{VOR UND B} alpha {NACH}
UND
{VOR UND NICHT(B)} beta {BACH}Ich befürchte das falsch gemacht zu haben :S
-
In den Schleifeninvarianten steht immer genau das gleiche drin, was auch die Schleife tut. Nur halt mathematisch notiert und nicht in der Programmiersprache. Wenn du also zuerst dein Code schreibst und dann Vor-/Nachbedingung und Schleifeninvariante aufstellst kannst du es auch bleiben lassen. Da du so nur bewiesen hast, dass deine kaputte Version das falsche Ergebnis liefert. Falls du deine Vor-/Nachbebedingungen aber zuerst aufstellest, dann kannst du durch die Schleifeninvariante beweisen, dass die Schleife deine Bedingungen erfüllt. Aber das heißt noch lange nicht, dass die Vor-/Nachbedingungen korrekt sind (Fehler bei der Interpretation der Spezifikation), oder die Spezifikation überhaupt korrekt ist.
