#12 Check for good style and completeness of specifications

[Joseph Kiniry]

The JML reference guide suggests various standards when
it comes to writing good specifications (or at least,
it starts to, I've been adding more information wrt
this area and I'll be committing it in the coming weeks).

I'd like an option on the checker to "lint check"
specifications to guarantee that they fulfill these
minimum obligations. Some bits recently added are
already along this path, though those mainly have to do
with correctness rather than style (e.g., pure method
checks, modifies visibility, etc.).

Basic examples of such checks are:
1. completeness of heavyweight specifications
(necessity of modifies clause, full coverage of
exceptional cases when a throws clause is present, full
coverage of pre-/post conditions, case analysis, etc.).
2. completeness of invariants (full coverage of all
attributes)
3. proper denotation of *redundantly specs (reference
checks via inhertiance)
4. constant use in specs (e.g., foo ==> bar when foo
is a static final)

You get the idea.