/*@ logic int my_log(real s) */ /*@ ensures \result == 2 ^^ (53) */ double malcolm1() { double A; A=2; /*@ assert A==2 */ /*@ invariant A== 2 ^^ my_log(A) && 1 <= my_log(A) <= 53 variant (53-my_log(A)) */ while (A != (A+1)) { A*=2; } return A; }
/*@ logic int my_log(real s) */ /*@ ensures \result == 2 ^^ (53) */ double malcolm1() { double A; A=2; /*@ assert A==2 */ /*@ invariant A== 2 ^^ my_log(A) && 1 <= my_log(A) <= 53 variant (53-my_log(A)) */ while (A != (A+1)) { A*=2; } return A; }