Menu

#99 Typecheck level 0 heavyweight spec cases

Level_0_support
open
nobody
JAJML (35)
3
2012-11-27
2009-06-05
No

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.

Discussion


Log in to post a comment.