# Schleifeninvariante bestimmen



## tim--97 (24. Jan 2017)

Hallo zusammen,
habe eine Aufgabe bei der ich nicht weiterkomme und leider auch nichts richtiges finden kann im Internet was mir hilft.
Gegeben ist folgender Algorithmus und ich soll mittels der Hoar`schen Regeln und der gegebenen Bedingungen die Korrektheit des Algrithmus beweisen. *Doch zuerst soll ich die Schleifeninvariante bestimmen* wo es bei mir schon hakt :/


```
{n >= 0}              --> Vorbedingung
       i = 0;
       s = 0;
       while (i < n) {
               s = s + n;
               i ++;
       }
{s == n * n}                           --> Nachbedingung
```

Bis jetzt habe ich eine Tabelle erstellt und _n = 5_ gesetzt:

```
s       i      n

0       0      5
5       1      5
10      2      5
15      3      5
20      4      5
25      5      5               --> letzter Schleifendurchlauf, da Schleifenbedingung nicht mehr erfüllt
```

Die Nachbedingung stimmt somit auch: 25 == 5 * 5
Als Schleifeninvariante fällt mir nur_ I = i * n_ ein aber dann habe ich Probleme bei dem Beweis.
Gibt es eine bessere Invariante?


----------

