Formal model of commands...
c, d ::= x = e; c d if (e) { c } else { d } while (e) { c }
and expressions...
e, f ::= x n e + f e == f ...
This is Smith and Volpano's model, dressed up in Java syntax.
