#20 Better test coverage features in JMLTestRunner

[David Cok]

The test coverage information produced by JMLTestRunner
could be improved:

- need to distinguish tests that contain non-executable
portions, especially those that masquerade as true

- would like to also report coverage of boolean terms
that make up a requires predicate

- when there is nesting using {| |} or implicit nesting
using non_null on arguments, the results can be
confusing. In the current implementation the outer
predicates are re-evaluated for each of the
preconditions inside the {| |}, so their test count is
some multiple of the real count. In the case of
non_null arguments, it needs to be clear to the user
that the test for null arguments is done first.

- currently JMLTestRunner directly calls a method in
JMLChecker. This creates a coupling that perhaps should
not be present. Some refactoring may be called for.

[David Cok]

Logged In: YES
user_id=595682

One more:

So far in the JML tools we have not used the nowarn
annotation. There is a good use for it here. There may be a
case where a test is always true or always false on the given
set for practical reasons (e.g. cannot make a collection of
Integer.MAX_VALUE size). A nowarn annotation could be used
to suppress unwanted warnings as in

//@ requires size() < Integer.MAX_VALUE; nowarn ALWAYS_TRUE;

[Gary T. Leavens]

Logged In: YES
user_id=633675

It might be nice to group all of the asserstions that are
always false and those that are always true. The false
preconditions indicate lack of test coverage.