Mult.java

public final class Mult {

   static int mult0 (final int a, final int b) {
      assert a >= 0 : String.format ("%d must not be negative", a);

      int x=a;
      int c=0;

      assert c + x*b == a*b : "loop invariant failed";
      assert x >= 0;

      while (x>0) {
         c = c + b;
         x = x - 1;

         // c + b + (x-1)*b = a*b
         assert c + x*b == a*b : "loop invariant failed";
         assert x >= 0;

      }

      assert x == 0;
      assert c == a*b : "method failed";
      return c;
   }
      
   static int mult (final int a, final int b) {
      assert a >= 0 : String.format ("%d must not be negative", a);

      int x = a, y = b, c = 0;

      assert c + x*y == a*b : "loop invariant failed";
      assert x >= 0;

      while (x > 0) {
         if (x%2 == 1) c += y;
         x /= 2;
         y *= 2;

         // c + y + x'*2*y = a*b ; if x=2*x'+1 (odd)
         // c + x'*2*y = a*b     ; if x=2*x'   (even)
         assert c + x*y == a*b : "loop invariant failed";
         assert x >= 0;
      }

      assert x == 0;
      assert c == a*b : "method failed";
      return c;
   }

   public static void main (String[] args) {
      final int a = Integer.parseInt (args[0]);
      final int b = Integer.parseInt (args[1]);
      System.out.printf ("%d * %d = %d%n", a, b, mult(a,b));
   }
}