#381 Invariants for Model Fields Ignored

[Eric Kerfoot]

I've noticed that invariants predicated on model fields seem to be ignored now.

The IntegerSetInterface interface in JML/org/jmlspecs/samples/sets directory of the JML distribution declares a model variable and states an invariant for it. The implementation IntegerSetAsHashSet provides a concrete implementation and a represents clause for the model variable.

When tests are run on IntegerSetAsHashSet with the invariant in the interface changed to something that is obviously wrong, no exception is thrown to indicate the invariant was checked.

Even if the invariant is copied into IntegerSetAsHashSet there seems to be no runtime check for the invariant, although method contracts continue to work as expected. If an invariant that states the exact same condition is given but stated for the concrete variable instead, this throws the correct exception.

This was suggested by Dr. Leavens to be a bug in jmlc since everything seems to be in place, and the problem has manifested in a known example, as well as my own code.