Model Car Security: Fortran Encoding




Three integer variables are used: s as speed for the speed, t as time for the seconds and d as distance for the estimated distance that the model car travels after loosing its track.
When the model car is erring, the maximum speed allowed is 2 meters per second and the maximum time is 3 seconds. The maximal distance travelled is 3 times 2 plus 3 for the last iteration. If the wall is 10 meter away from the track, the model car will never crash into it.
These numerical constants could be changed, but have to be known numerically at analysis time to keep the invariants in the affine relationship set.


      program voiture02

C     Test de l'arret de la voiture propose par Nicolas Halbwachs, 15
C     mars 2005

      integer s, t, d

      s = 0
      t = 0
      d = 0

      do while(s.le.2.and.t.le.3)
         read *, x
         if(x.gt.0.) then
            t = t + 1
            s = 0
         else
            d = d + 1
            s = s + 1
         endif
      enddo

      print *, s, t, d
      read *, t, s

      if(d.le.10) then
         print *, "healthy"
      else
         print *, "crashed!"
      endif

      end