Schleifeninvariante finden für Beweis von Schleife(?)

Neue Frage »

Auf diesen Beitrag antworten »
tftm 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?
 
 
Neue Frage »
Antworten »


Verwandte Themen

Die Beliebtesten »
Die Größten »
Die Neuesten »