Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
WP-Kalkül SS 2011
Ich habe eine Frage zur SS 2011 (Seite 17, Aufgabe 6c).
Folgender Code war gegeben:
long cpIter(long n) {
long a = 1, k = n-1, p=1;
if (n > 0) {
while (k > 0) {
p *= 2;
k--;
}
a = (n+2) * p;
}
return a;
}
Man sollte beweisen, dass die gewählte Schleifeninvariante “p = 2^(n-k-1) && k >=0” unmittelbar vor dem ersten Betreten des Schleifenrumpfs gilt.
Die FSI-Lösung: https://fsi.cs.fau.de/dw/pruefungen/bachelor/aud/loesungss11#aufgabe_6_-_formale_verifikation
wp("a = 1; k = n - 1; p = 1; if(n > 0)", p = 2^(n - k - 1) ∧ k ≥ 0) =
[(n > 0) ∧ wp("a = 1; k = n - 1; p = 1;", p = 2^(n - k - 1) ∧ k ≥ 0)] ∨ [n ≤ 0] =
...
Warum muss am Ende “n <= 0” noch stehen? Damit die Invariante gilt, muss doch n > 0 gewesen sein. In jedem anderen Fall wird die while-Schleife erst gar nicht erreicht.
Die IF/ELSE-Regel ist mir bekannt, nur ist es hier so, dass man vom Inneren eines IFs heraus sich nach oben arbeitet 
Die ersten zwei Zeilen aus der in der Vorlesung gezeigten Lösung lauten:
wp("a = 1; k = n - 1; p = 1; if(n > 0) { ...", p = 2^(n - k - 1) ∧ k ≥ 0)
= wp("a = 1; k = n - 1; p = 1", [n > 0 ∧ p = 2^(n - k - 1) ∧ k ≥ 0] ∨ [n ≤ 0 ∧ true])
...
Spielt hier die andere Reihenfolge der wp()-Funktion eine Rolle?
Aber auch hier dieselbe Frage wie oben: Warum n <= 0?
wurde glaub ich hier auch schon mal gefragt:
https://fsi.cs.fau.de/forum/thread/8821-Klausur-11-08-2011-Aufgabe-6-c-wp
Wenn ich den Rat von blabori in dem verlinkten Thread befolge, gelingt mir der Beweis nicht.
Zu zeigen: n >= 0 => wp(„a := 1; k := n-1; p := 1; if (n > 0) {…“, p=2^(n-k-1) && k >= 0)
(n >= 0 => wp("a := 1; k := n-1; p := 1; if (n > 0) {...", p=2^(n-k-1) && k >= 0))
<=> (n >= 0 => wp("a := 1; k := n-1; p := 1", n > 0 && p=2^(n-k-1) && k >= 0))
<=> (n >= 0 => wp("a := 1; k := n-1", n > 0 && 1=2^(n-k-1) && k >= 0))
<=> (n >= 0 => wp("a := 1", n > 0 && 1=2^(n-(n-1)-1) && n-1 >= 0))
<=> (n >= 0 => wp("a := 1", n > 0 && 1=2^(0) && n-1 >= 0))
<=> (n >= 0 => wp("a := 1", n > 0 && n-1 >= 0))
<=> (n >= 0 => n > 0 && n-1 >= 0)
<=> (n >= 0 => n > 0 && n >= 1)
<=> (n >= 0 => n >= 1)
Aus n >= 0 folgt sicher nicht n >= 1.
Anscheinend muss der else-Fall doch behandelt werden! Aber warum?
Wird bei uns das wp kalkül nicht immer verwendet um “nachzuweisen”, dass eine bestimmte Methode korrekt arbeitet? Sprich alle möglichen Eingabewerte müssen überprüft werden?