Model Car Security: PIPS Transformers




The elementary and compound commands of the program are automatically abstracted by polyhedra. With the options selected, the abstract commands include some precondition information. It is sufficient to show that the model car will never crash.



C  T() {}

      PROGRAM VOITURE02

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

      INTEGER S, T, D

C  T(D,S,T) {0<=D, D<=9}

C     BEGIN BLOCK

C  T(S) {S==0}

      S = 0                                                             0001

C  T(T) {S==0, T==0}

      T = 0                                                             0002

C  T(D) {D==0, S==0, T==0}

      D = 0                                                             0003

C  T(D,S,T) {D#init<=D, D+S#init+2T#init<=D#init+S+2T, T#init<=T}

      DO WHILE (S.LE.2.AND.T.LE.3)                                      0004

C  T(D,S,T) {D+T==D#init+T#init+1, S#init+3T#init+1<=S+3T,
C    S+3T<=3T#init+3, S#init<=2, T#init<=T, T<=T#init+1, T#init<=3}

C        BEGIN BLOCK

C  T() {S<=2, T<=3}

         READ *, X                                                      0005

C  T(D,S,T) {D+T==D#init+T#init+1, S#init+3T#init+1<=S+3T,
C    S+3T<=3T#init+3, T#init<=T, T<=T#init+1, T#init<=3}

         IF (X.GT.0.) THEN                                              0006

C  T(S,T) {S==0, T==T#init+1, S#init<=2, T<=4}

C           BEGIN BLOCK

C  T(T) {T==T#init+1, S<=2, T<=4}

            T = T+1                                                     0007

C  T(S) {S==0, S#init<=2, T<=4}

            S = 0                                                       0008
C           END BLOCK
         ELSE

C  T(D,S) {D==D#init+1, S==S#init+1, S<=3, T<=3}

C           BEGIN BLOCK

C  T(D) {D==D#init+1, S<=2, T<=3}

            D = D+1                                                     0009

C  T(S) {S==S#init+1, S<=3, T<=3}

            S = S+1                                                     0010
C           END BLOCK
         ENDIF
C        END BLOCK
      ENDDO

C  T() {0<=D, S<=3D, D<=S+2T, 1<=D+T, S<=3, S+3T<=12, 0<=T, T<=4}

      PRINT *, S, T, D                                                  0011

C  T(S,T) {0<=D, S#init<=3D, D<=S#init+2T#init, 1<=D+T#init,
C    S#init<=3, S#init+3T#init<=12, 0<=T#init, T#init<=4}

      READ *, T, S                                                      0012

C  T() {0<=D, D<=9}

      IF (D.LE.10) THEN                                                 0013

C  T() {0<=D, D<=9}

         PRINT *, "healthy"                                             0014
      ELSE

C  T() {0==-1}

         PRINT *, "crashed!"                                            0015
      ENDIF

C     END BLOCK
      END