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 :/
Bis jetzt habe ich eine Tabelle erstellt und n = 5 gesetzt:
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?
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 :/
Java:
{n >= 0} --> Vorbedingung
i = 0;
s = 0;
while (i < n) {
s = s + n;
i ++;
}
{s == n * n} --> NachbedingungBis jetzt habe ich eine Tabelle erstellt und n = 5 gesetzt:
Code:
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ülltDie 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?
