Model Car Security: Preconditions




Since the preconditions can be computed together with the transformers in this case, no information is added, but the precondition information is easier to read.



C  P() {}

      PROGRAM VOITURE02

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

      INTEGER S, T, D

C  P() {}

C     BEGIN BLOCK

C  P() {}

      S = 0                                                             0001

C  P(S) {S==0}

      T = 0                                                             0002

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

      D = 0                                                             0003

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

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

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

C        BEGIN BLOCK

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

         READ *, X                                                      0005

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

         IF (X.GT.0.) THEN                                              0006

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

C           BEGIN BLOCK

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

            T = T+1                                                     0007

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

            S = 0                                                       0008
C           END BLOCK
         ELSE

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

C           BEGIN BLOCK

C  P(D,S,T) {0<=D, S<=3D, S<=2D+2T, D<=S+2T, S<=2, 0<=T, T<=3}

            D = D+1                                                     0009

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

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

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

      PRINT *, S, T, D                                                  0011

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

      READ *, T, S                                                      0012

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

      IF (D.LE.10) THEN                                                 0013

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

         PRINT *, "healthy"                                             0014
      ELSE

C  P() {0==-1}

         PRINT *, "crashed!"                                            0015
      ENDIF

C     END BLOCK
      END