| static int div(int x, int y){
// require x > 0 && y > 0;
int rest = x;
int quotient = 0;
while (rest >= y) {
// invariant rest + quotient * y = x;
// System.out.println(rest + quotient * y == x);
rest = rest - y;
quotient = quotient + 1;
}
return (quotient);
// ensure rest + quotient * y = x && rest < y && rest >= 0;
} // end div |
|
| | Et eksempel på en iterativ funktion med en løkke invariant.
|