translation scheme

Java statement to logical formula

Sn : stmt ? formula

n is # loop iters

Java term to set/relation expression

E : term ? expr

Java predicate to formula

P : pred ? formula

Previous slide

Next slide

Back to first slide

View graphic version