a policy
System specified in Java
Iterative refinement with feedback from compiler
Refined until model compliant
Next Slide
