#118 More information about model fields is needed in JMLRAC

[Clyde D. Ruby]

When specifications fail to pass the checking done by
JMLRAC, the improved information about the state of
concrete fields and objects is very helpful when
debugging the implementation.
However, when there is a problem with the specification,
this information doesn't help as much. That is, the value
of model fields and objects need to be printed also.
Sometimes some of the values of model fields and objects
are printed but not often enough. That is, printing the
state of ALL the model fields and objects would be better
in my opinion. Thus both the concrete and model values
are needed to have any idea where things are going
wrong when things get complicated. This is especially
true since there is no way to print the state of a model
object since it cannot be accessed in the body of a
concrete method. For example, when there is a problem
with a complicated represents clause, there is no way to
see the values of the model fields of the class. This is
critical when debugging the specifications!!
I didn't see this feature request so perhaps no one has
used JMLRAC on a set of classes that have complex
interactions between the model fields of several different
classes. Sometimes I have been able to use JML's assert
statement to force JMLRAC to print the value of a model
field, but usually what I need doesn't get printed (and it
can be very frustrating).
Again, the usefulness of the messages generated by
JMLRAC are much improved. But more information about
model fields is needed!

[Gary T. Leavens]

Logged In: YES
user_id=633675

Francisco Laguna writes:

I would like JML (or, more precisely, jmlc and jmlrac ) even
more, if they
would give me more information on a failure. Consider the
following JML:

/*@
@ public normal_behavior
@ requires 0 <= index && index <= size();
@
@ ensures
@ size() == \old(size())+1 && itemAt(index) == i;
@
@*/
public void insert(int index, int i){
...
}

Once the Postcondition is violated I get the following output:
------snip----
Exception in thread "main"
org.jmlspecs.jmlrac.runtime.JMLNormalPostconditionError: by
method
MyLinkedList.insert regarding specifications at
File "workspace/DBC/MyLinkedList.java", line 99, character 23
when
'i' is 3
'\old(size())' is 0
'index' is 0
'this' is MyLinkedList@c9a690
.
.
.
----------------

The value of 'size()' and itemAt(index) (or in short, the left
side of the
conditions), would also be helpful for diagnosing the problem.
Those would
also point me precisely at what part of the condition had
been violated.
While trying out JML by implementing a linked list, I
continually had to
start outputting variables just to find out, which part of my
specification
had been violated.