Operational semantics for finally blocks?
Note that the Java issue with return statements does not appear here.
