---

Geschrieben von tftm am 12.04.2018 um 14:25:

  Schleifeninvariante finden für Beweis von Schleife(?)

Meine Frage:
Wir müssen in einer Aufgabe zeigen, dass bei folgendem Programm unter der Vorbedingung n ? 1 die Nachbedingung y=??n? gilt.

Dazu sollten wir die Notation "Proof-carrying code" benutzen, um die Korrektheit und Terminierung des Programmes zeigen, dafür braucht man aber eine Schleifeninvariante, welche ich nicht finde.

public int foo(int n) {
int y = 0;
while ( y*y < n ) {
y = y + 1;
}
}


Meine Ideen:

Weiss da jemand weiter?