7. Verification - Continued
The two remaining specification features each attach a contract to something other than a procedure's normal return: an exceptional exit, and a coroutine's suspension points. Both build on everything above — postconditions for what a contract is, and frames for what may change — so they come last.
The constructs themselves are execution features, described under
Execution: throws / throw / try / catch / finally under
Exceptions, and coroutine / yield / resume under Coroutines.