This task should be done _after_ the similar task for lightweight spec
cases.
From the JML Ref Manual: Heavyweight specification cases (see section 9.5
Heavyweight Specification Cases) that do not use the keyword code. This
includes behavior-spec-case (see section 9.6 Behavior Specification
Cases),
normal-behavior-spec-case (see section 9.7 Normal Behavior Specification
Cases), and exceptional-behavior-spec-case (see section 9.8 Exceptional
Behavior Specification Cases). However, note that not all clauses that are
allowed in the syntax are in level 0.