KB3D example

The following example is an excerpt of the KB3D program for aircraft conflict detection and resolution, designed at NIA.

Using Frama-C/Jessie with the multirounding model described in this paper, we are able to verify this program independently of the underlying compiler and architecture

#pragma JessieFloatModel(multirounding)
#pragma JessieIntegerModel(math)

//@ logic integer l_sign(real x) = (x >= 0.0) ? 1 : -1;

/*@ requires e1<= x-\exact(x) <= e2;   
  @ ensures  (\result != 0 ==> \result == l_sign(\exact(x))) &&
  @          \abs(\result) <= 1 ;
  @*/
int sign(double x, double e1, double e2) {
  if (x > e2)
    return 1;
  if (x < e1)
    return -1;
  return 0;
}
 
/*@ requires 
  @  sx == \exact(sx)  && sy == \exact(sy) &&
  @  vx == \exact(vx)  && vy == \exact(vy) &&
  @  \abs(sx) <= 100.0 && \abs(sy) <= 100.0 && 
  @  \abs(vx) <= 1.0   && \abs(vy) <= 1.0; 
  @ ensures
  @  \result != 0 
  @    ==> \result == l_sign(\exact(sx)*\exact(vx)+\exact(sy)*\exact(vy))
  @         * l_sign(\exact(sx)*\exact(vy)-\exact(sy)*\exact(vx));
  @*/

int eps_line(double sx, double sy,double vx, double vy){
  int s1,s2;

  s1=sign(sx*vx+sy*vy, -0x1.9a0641p-45, 0x1.9a0641p-45);
  s2=sign(sx*vy-sy*vx, -0x1.9a0641p-45, 0x1.9a0641p-45);
 
  return s1*s2;
}

This is proved by a combination of automated provers: SMT solvers (CVC3 and Alt-Ergo) and Gappa, as shown by the following GWhy screenshot.