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 Folie uebung 9 fibonaci
Irgendwie komm ich nciht auf die Lösung: also die schritte sind ja
- zeigt das I vor der schleife gilt
- zeige das I whärend der Schleife gilt,
- zeige das die schleife terminiert.
I = f=F_i AND fn = F_i+1
wp(i = 0; f = 1; fn = 1;", f=F_i AND fn = F_i+1)
= (1 = 1 And 1 = 1) = true den rechenweg spar ich mal
wp(“tmp = f + fn; f = fn; fn = tmp; i++;”, f=F_i+1 AND fn = F_i+1
wp(“tmp = f + fn; f = fn; fn = tmp;”, f= F_i+1 AND fn = F_i+2
wp("tmp = f + fn; f = fn; ",f= F_i+1 AND tmp = F_i+2
wp("tmp = f + fn;"fn= F_i+1 AND tmp = F_i+2
=(fn= F_i+1 AND f + fn = F_i+2)
So jetzt meine Frage, müsste da nciht die Schleifeninvariante rauskommen?
Die Invariante ist nicht f=F_n …, sondern f=F_i … .
war ein Tippfehler. hmm aber ändert nichts am problem: hhmm
wird fn = F_i+1 AND f + fn = F_i+2 umgeform zu f = Fn? Da {fn = F_i+1} = true, gilt das auch für f + fn = F_i+2, daher bleibt dann nur noch f = F_i übrig und da i = n die abbruchbedingung ist, bleibt eben f = F_n als Nachbedingung erfüllt??? Glaube es irgendwie zu verstehen und irgendwie auch wieder nicht. 
Das stimmt und jetzt siehst du, dass nach der Schleife die Bedingung f = F_i und fn = F_i+1 gilt. Das ist gerade deine Bedingung, die vor der Schleife gilt. Also ist diese Bedingung in der Tat eine Invariante.
Das ist auch richtig und somit ist die Schleife partiell korrekt.