Sylvie Boldo

Gallery of proved programs

	⇑
⇐	Screenshot of gWhy	⇒
	Screenshot of Why3

KB3D: an avionics example

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. The proofs are here fully automatic.

#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;
}