Verification of Compilers - Correct System Design: Recent Insights and Advances - page 207

cond cond

NT NT NT NT NT

NT

any 1 any 2 any 1 any 2

EXPR WHILE EXPR WHILE

TT

TT

NT

STATS EXPR does not

contain function calls

STATS is not empty

EXPR does not
contain function calls

L1:
ifjmp(EXPR,L1,L2)

L2:

NT

any 1 any 2

L2:

NT

any 1 any 2

ifjmp(EXPR,L1,L2)

NT

L1:

src

NT NT

any 1 any 2

DES EXPR ASSIGN

dest

EXPR.type=int
EXPR does not contain function calls

DES.type=int

any 1 any 2

intassign(DES,EXPR)

π y

x y

refuse x