1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:
31:
32:
33:
34:
35:

function p(n:Integer):Integer {

    // Precondition: Unsere Variable result enthält zu Beginn der Iteration 
    // den Wert 0 und n >= 2. (Der Fehler, den Friedrich beschrieben hat, 
    // fangen wir hier nicht ab. In dem Fall wird 0 zurückgegeben). Das ist 
    // die Ausgangssituation vor der Iteration.
    result = 0;     

    while (n > 3) {
         // Invariante: Sagt aus, was zum Zeitpunkt eines Iterationsschrittes
         // als Bedingung in der Schleife gegeben sein muss. Hier ist die
         // Bedingung lediglich, dass n > 3 gegeben sein muss. Die Bedingung 
         // n > 3 kommt daher, weil wir uns vom rekursiven Term zu den
         // anderen hangeln.

         ...
    }
    // Postcondition: result = result + 2n+1 (zusammengefasst) und n = n-1
    // Die Nachbedingung, beschreibt den Zustand nach einem Iterations-
    // schritt.

    // Jetzt kümmern wir uns um die anderen und restlichen Fälle:
    // Die stärkere Bedingung zuerst.
    if (n == 3) {
        result = result + 1;
    }

    // Da wir am Anfang result schon mit 0 initialisiert haben, haben wir den
    // Fall, dass n==2 ist bereits abgedeckt. Auch wenn wir in der Schleife
    // gewesen sind, dann wird ja nichts dazuaddiert. Also einfach result
    // zurückgeben.
    return result;
}