1978 Historical Example by Cousot and Halbwachs: Transformers by PIPS





C  T() {}

      PROGRAM CH78

C  T(I,J) {6<=I+2J, 2J+2<=I, 0<=J}

C     BEGIN BLOCK

C  T(I) {I==2}


C     POPL 78, example in Section 5

      I = 2                                                             0001

C  T(J) {I==2, J==0}

      J = 0                                                             0002

C  T(I,J) {I#init+2J<=I+2J#init, J#init<=J}


      DO WHILE (X.GT.0.)                                                0003

C  T(I,J) {I+2J==I#init+2J#init+4, I#init+2<=I, I<=I#init+4}

C        BEGIN BLOCK

C  T(I,J) {I+2J==I#init+2J#init+4, I#init+2<=I, I<=I#init+4}

         IF (Y.GT.0.) THEN                                              0004

C  T(I) {I==I#init+4}

            I = I+4                                                     0005
         ELSE

C  T(I,J) {I==I#init+2, J==J#init+1}

C           BEGIN BLOCK

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

            J = J+1                                                     0006

C  T(I) {I==I#init+2}

            I = I+2                                                     0007
C           END BLOCK
         ENDIF

C  T() {}

         PRINT *, I, J                                                  0008
C        END BLOCK
      ENDDO

C     END BLOCK
      END


Go back to the Fortran input code or see the preconditions