Here are a few exercises for understanding translation rules from
Java to Why.
Here is a proposal for a simple rule for translating field
| [[e.f++]]||=||[[e.f = e.f+1]]|
Show why it is not correct, and propose a correct translation rule.
- Propose a translation rule for the for loop:
for(e1 ; e2 ; e3) s
- Propose translation rules for break and
continue with labels, and modify translation rule of the
while loop accordingly.
- Propose translation rules for the switch statement.
This document was translated from LATEX by