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