KB3D: an avionics example

This avionics code has been modified to take into account floating-point inaccuracies.

Authors: Sylvie Boldo / Thi Minh Tuyen Nguyen

see also the index (by topic, by tool, by reference, by year)

This example is part of KB3D, an aircraft conflict detection and resolution program. The aim is to make a decision corresponding to value -1 and 1 to decide if the plane will go to its left or its right. Note that KB3D is formally proved correct using PVS and assuming the calculations are exact. However, in practice, when the value of the computation is small, the result may be inconsistent or incorrect.

#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, -0x1p-45, 0x1p-45);
  s2=sign(sx*vy-sy*vx, -0x1p-45, 0x1p-45);
 
  return s1*s2;
}

/* 
Local Variables:
compile-command: "LC_ALL=C make eps_line"
End:
*/

Toccata

Formally Verified Programs, Certified Tools and Numerical Computations

KB3D: an avionics example