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