tftm
Grünschnabel
Dabei seit: 12.04.2018
Beiträge: 1
 |
|
| 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?
|
|
