#10 Usage and output improvements for jmlc

[David Cok]

The jmlc has useful output messages that have been
invaluable in debugging specifications. Here are some
additional suggestions.

- The more detail the better on which part of which
specification clause is failing with which test. The
computed values of various portions of the specification
expressions would be useful - e.g. the two terms being
compared in a relational operation or the various
arguments of logical operations.

- An easy case to call out more clearly is that of an
exception being received in a normal_behavior block.

- Nonexecutable constructs such as missing model methods
can cause tests to succeed or fail inexplicably. It
would be better to at least have warning messages
generated for these cases, if not outright errors.

- It would be helpful to have detail regarding which
requires clauses (and portions of such clauses) are
always true or always false, in order to be able to
write tests that more completely cover the specification
space.

- In some cases, if a test is not meaningful it means
that there are missing cases in the specifications. It
would be helpful to be able to obtain detail on which
tests are not meaningful for which methods.

- The generated code could have its performance improved
by identifying common subexpressions - there can be
quite a bit of duplicate computation. An easy case
might be that of a requires clause that precedes a {| |}
block.

[David Cok]

Logged In: YES
user_id=595682

An option (-M) has been added to JMLTestRunner. When
utilized, information regarding test cases declared
meaningless is listed at the end of the test run. - DRCok