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.
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
read *, x
t = t + 1
s = 0
d = d + 1
s = s + 1
print *, s, t, d
read *, t, s
print *, "healthy"
print *, "crashed!"