Sylvie Boldo

Gallery of proved programs

Average of two floating-point numbers, correct version

This function computes the correct rounding of the average of two floating-point numbers. It gives the perfect value, while preventing overflows.

/*@ ensures \result == \abs(x); */
double abs(double x) {
  if (x >= 0) return x;
  else return (-x);
}


/*@   requires 0x1p-967 <= C <= 0x1p970; 
  @   ensures \result == \round_double(\NearestEven, (x+y)/2) ;
  @ */

double average(double C, double x, double y) {
  if (C <= abs(x)) 
    return x/2+y/2;
  else
    return (x+y)/2;
}