N
neuer Nutzer
Gast
Ich habe ein Problem mit einer Aufgabe bzw. Beweis über die Verifikation zu einer if Anweisung.
Folgender Programmtext ist gegeben:
Gegeben ist noch die Vorbedingung: b>0 sowie die Nachbedingung c>=2.
Wir haben folgende Beweismethode gewählt. Und zwar sollen wir von der Nachbedingung zur Vorbedingung folgern.
Das würde also so aussehen:
Um zu zeigen, dass die Vorbedinung if B {alpha} else {beta} Nachbedingung gilt, soll man zeigen:
{Vorbedingung und B} alpha {Nachbedingung} sowie{Vorbedingung und B negiert} beta {Nachbedingung}.
Das habe ich angewendet:
Betrachten wir einmal nur den else-Zweig. Vielleicht genügt mir das schon, um es zu verstehen. Ich weiß also, dass die Nachbedingung c>=2 lautet. Das bedeutet, dass a+1>=2 gelten muss. Also umgeformt: a>=1. Jetzt komme ich dann zu dem Text: "a=3*a+b". Wie kann ich nun weiter folgern? Wäre dies hier korrekt: Ich weiß nun, dass a>=1 gilt. Also muss 3*a+b>=1 sein. Nur wie kommt man nun auf die Vorbedingung, dass b>0 sein soll und a<=0?
Folgender Programmtext ist gegeben:
Java:
if (a > 0) {
a = a + 2 * b;
c = a / 2 + 1;
} else {
a = -a;
a = 3 * a + b;
c = a + 1;
}
Gegeben ist noch die Vorbedingung: b>0 sowie die Nachbedingung c>=2.
Wir haben folgende Beweismethode gewählt. Und zwar sollen wir von der Nachbedingung zur Vorbedingung folgern.
Das würde also so aussehen:
Java:
{b>0}//Vorbedingung
if (a > 0) {
a = a + 2 * b;
c = a / 2 + 1;
}else{
a = -a;
a = 3 * a + b;
c = a + 1;
}
{c>=2}//Nachbedingung
Um zu zeigen, dass die Vorbedinung if B {alpha} else {beta} Nachbedingung gilt, soll man zeigen:
{Vorbedingung und B} alpha {Nachbedingung} sowie{Vorbedingung und B negiert} beta {Nachbedingung}.
Das habe ich angewendet:
Java:
{b>0}
if (a > 0) {
{b>0 und a>0}
a = a + 2 * b;
{a/2 +1>=2}
c = a / 2 + 1;
{c>=2}
}else{
{b>0 und a <= 0}
a = -a;
a = 3 * a + b;
{a+1>=2}
c = a + 1;
{c>=2}
}
{c>=2}
Zuletzt bearbeitet von einem Moderator: