loop-invariants/1/instrumented-div.cs - Division by repeated subtraction - instrumented with output inside loop.

Lecture 13 - slide 32 : 32 Program 3

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));
  }

}