| using System;
class LoopInvariantDemo{
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;
Console.WriteLine("{0,-3} + {1,-3} * {2,-3} = {3,-3}",
rest, quotient, y, x);
rest = rest - y;
quotient = quotient + 1;
}
Console.WriteLine("{0,-3} + {1,-3} * {2,-3} = {3,-3}",
rest, quotient, y, x);
return quotient;
// ensure rest + quotient * y = x && rest < y && rest >= 0;
}
public static void Main(){
Console.WriteLine("Div({0}, {1}) = {2}\n", 10, 2, Div(10, 2));
Console.WriteLine("Div({0}, {1}) = {2}\n", 11, 2, Div(11, 2));
Console.WriteLine("Div({0}, {1}) = {2}\n", 100, 25, Div(100, 25));
}
} |