Here are a few exercises for understanding translation rules from Java to Why.

1. Here is a proposal for a simple rule for translating field incrementation:

   [[e.f++]] = [[e.f = e.f+1]]

   Show why it is not correct, and propose a correct translation rule.

2. Propose a translation rule for the for loop:
   for(e₁ ; e₂ ; e₃) s
3. Propose translation rules for break and continue with labels, and modify translation rule of the while loop accordingly.
4. Propose translation rules for the switch statement.

This document was translated from L^AT_EX by H^EV^EA.