Leaking Gaz Burner: 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 leaking rate is under the required limit.
Note that the program transformer is empty because the program never terminates. And that the transformer information is not sufficient to decide if the maximal leakage will be reached or not. Preconditions must be computed too.


C  T() {0==-1}

      PROGRAM GAZ_BURNER02

C     Check maximum leaking rate of a gaz burner: Nicolas Halbwachs and Laure Gonnord

      INTEGER T, L, X
      EXTERNAL ALEA
      LOGICAL ALEA

C  T() {0==-1}

C     BEGIN BLOCK

C  T(T) {T==0}


      T = 0                                                             0001

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

      L = 0                                                             0002

C  T(X) {L==0, T==0, X==0}

      X = 0                                                             0003

C  T(L,T,X) {X==X#init, L#init<=L, 6L+T#init<=6L#init+T}

      DO WHILE (.TRUE.)                                                 0004

C  T(L,T,X) {X==0, L#init+1<=L, L+T#init+50<=L#init+T,
C    L+X#init<=L#init+10}

C        BEGIN BLOCK

C  T(L,T,X) {L+X#init==L#init+X, T+X#init==T#init+X, T#init<=T}

         DO WHILE (X.LE.9.AND.ALEA())                                   0005

C  T(L,T,X) {L==L#init+1, T==T#init+1, X==X#init+1, X<=10}

C           BEGIN BLOCK

C  T(T) {T==T#init+1, X<=9}

            T = T+1                                                     0006

C  T(L) {L==L#init+1, X<=9}

            L = L+1                                                     0007

C  T(X) {X==X#init+1, X<=10}

            X = X+1                                                     0008
C           END BLOCK
         ENDDO

C  T(X) {X==0, X#init<=10}

         X = 0                                                          0009

C  T(T,X) {T+X#init==T#init+X, T#init<=T}

         DO WHILE (X.LE.49.OR.ALEA())                                   0010

C  T(T,X) {T==T#init+1, X==X#init+1}

C           BEGIN BLOCK

C  T(T) {T==T#init+1}

            T = T+1                                                     0011

C  T(X) {X==X#init+1}

            X = X+1                                                     0012
C           END BLOCK
         ENDDO

C  T(X) {X==0, 50<=X#init}

         X = 0                                                          0013

C  T() {X==0}

C        Check the leakage rate
         IF (6*L.GT.T+50) THEN                                          0014

C  T() {X==0, T+51<=6L}

            PRINT *, "unsafe"                                           0015
         ELSE

C  T() {}

C           BEGIN BLOCK
C           END BLOCK
         ENDIF
C        END BLOCK
      ENDDO

C     END BLOCK
      END