Malcolm algorithm to determine the radix
How to determine the radix using only floating-point computations.
Auteurs: Sylvie Boldo
Catégories: Floating-Point Computations
Outils: Frama-C / Jessie / Coq
Références: NSV-3 Benchmarks
see also the index (by topic, by tool, by reference, by year)
This function computes the radix of the floating-point computations using only floating-point computations. Here in IEEE-754 double precision, the result is 2. The fact that the while (A != (A+1)) loop terminates is also proved.
/*@ ensures \result == 2.; */
double malcolm1() {
double A, B;
A=2.0;
/*@ ghost int i = 1; */
/*@ loop invariant A== \pow(2.,i) &&
@ 1 <= i <= 53;
@ loop variant (53-i); */
while (A != (A+1)) {
A*=2.0;
/*@ ghost i++; */
}
/*@ assert i==53 && A== 0x1.p53; */
B=1;
/*@ ghost i = 1;*/
/*@ loop invariant B == i && (i==1 || i == 2);
@ loop variant (2-i); */
while ((A+B)-A != B) {
B++;
/*@ ghost i++; */
}
return B;
}