Frage:
Ich gehe grad mit einem Kollegen alte Aufgaben durch und weiß beim besten Willen nicht wie man die Schleifeninvariante beweisen soll.
Aufgabenstellung ist wie folgt:
Zeigen Sie, dass die definierte Schleifeninvariante in jedem Bereich der gegebenen Schleife gilt:
Vor dem Betreten der Schleife, vor und nach dem Ausfuhren des Rumpfes und nach dem Ver- ¨
lassen der Schleife.
Ich dachte, dass durch die requires und ensure bereits festgelegt wird, dass vor und nach der Ausführung die Vorrasussetzungen gegeben sind. In diesem Fall wäre es ja solange ein Feld vor victor frei ist kann er sich fortbewegen.
Code:
@requires field in front of victor is free
* @ensures victor has moves 1 field forward
* @loop_invariant victor visited i field
* @decreasing 5-i
private void multiMove(Integer times) {
for(int i = 0 ;i < 5; i++)
victor.move();
