1978 Historical Example by Cousot and Halbwachs: Preconditions by PIPS

Preconditions in the paper are labelled: {0} for the program input precondition, {1} at loop entry (line 003), {2}, [3}, {5} (lines 004, 005 and 006), {4} (not shown), {6} (not shown), {7} (line 008).

C  P() {}

      PROGRAM CH78

C  P() {}

C     BEGIN BLOCK

C  P() {}


C     POPL 78, example in Section 5

      I = 2                                                             0001

C  P(I) {I==2}

      J = 0                                                             0002

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

      DO WHILE (X.GT.0.)                                                0003

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

C        BEGIN BLOCK

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

         IF (Y.GT.0.) THEN                                              0004

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

            I = I+4                                                     0005
         ELSE

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

C           BEGIN BLOCK

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

            J = J+1                                                     0006

C  P(I,J) {2J<=I, 1<=J}

            I = I+2                                                     0007
C           END BLOCK
         ENDIF

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

         PRINT *, I, J                                                  0008
C        END BLOCK
      ENDDO

C     END BLOCK
      END

Go back to the Fortran input code or to the transformers