public class Mul { /*@ @ requires b>=0; @ ensures \result == a*b; @*/ public static int mul(int a, int b) { int sum = 0; /*@ loop_invariant sum + a*b == a*\old(b); @ assignable sum,b; @ decreases b; @*/ while (b > 0) { sum += a; b--; } return sum; } }