Java Modeling Language (JML)

Can you send the details of one of the tests that is failing?  It seems 
that there is a runtime error being raised during the evaluation of an 
assertion (recall that definedness checking is now the default).

Joseph Kiniry wrote:
> Hi all,
>
> I am attempting to re-run some old extensive unit tests in JML 5.5.   
> Hundreds of my tests are failing with traces akin to:
>
> Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid  
> Expression in "<GENERATED-BY-mjc>", line 0, character 0
> JMLEvaluationError cause: class  
> org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError
>
> Anyone recognize this offhand?
>
> Joe
>   
-- 
Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof.
Dependable Software Research Group, CSE Department, Concordia University
Room EV3.215, Phone +1-514-848-2424 x3004. http://www.encs.concordia.ca/~chalin

On 15 Jul, 2008, at 18:37, Patrice Chalin wrote:

> Can you send the details of one of the tests that is failing?  It  
> seems that there is a runtime error being raised during the  
> evaluation of an assertion (recall that definedness checking is now  
> the default).

Hrm.

E.g., in the KOA tally system, AuditLog's class initializer is  
failing.  Unfortunately, none of its invariants are under-defined.

https://trac.ucd.ie/trac/browser/software/evoting/koa/trunk/plugins/DutchTallySystem/src/sos/koa/AuditLog.java

The bogus instance invariant on the field kiesKringen has been removed  
in my sandbox.

Joe

> Joseph Kiniry wrote:
>> Hi all,
>>
>> I am attempting to re-run some old extensive unit tests in JML  
>> 5.5.   Hundreds of my tests are failing with traces akin to:
>>
>> Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid   
>> Expression in "<GENERATED-BY-mjc>", line 0, character 0
>> JMLEvaluationError cause: class   
>> org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError
>>
>> Anyone recognize this offhand?
>>
>> Joe

Patrice et al,

On 15 Jul, 2008, at 18:37, Patrice Chalin wrote:

> Can you send the details of one of the tests that is failing?  It  
> seems that there is a runtime error being raised during the  
> evaluation of an assertion (recall that definedness checking is now  
> the default).

After further investigation with both jProfiler and the Eclipse  
debugger, I'm guessing that the problem is perhaps related to an  
interaction between the new definedness checking and JML-junit.  I  
suspect that JML-junit has not being upgraded to support the new  
default behavior of programs compiled with jmlc, because as far as I  
recall, there are no jml-junit system tests in JML4.

Are the old assertion semantics completely gone from JML >= 5.5?  I  
see no command-line switch to trigger old behavior.

I am struggling with this new behavior in the general.  E.g., when I  
attempt to run the tally application within jmlrac 5.5 I see failures  
as well in class initializers for classes that have no invariants.

I am now reinstalling JML 5.4 and 5.3 to test against those releases.

I can provide a workspace snapshot, of course, for others to have a  
look at.  It is over 150MB when uncompressed through, as it is the  
full KOA workspace.

Joe

> Joseph Kiniry wrote:
>> Hi all,
>>
>> I am attempting to re-run some old extensive unit tests in JML  
>> 5.5.   Hundreds of my tests are failing with traces akin to:
>>
>> Caused by: org.jmlspecs.jmlrac.runtime.JMLEvaluationError: Invalid   
>> Expression in "<GENERATED-BY-mjc>", line 0, character 0
>> JMLEvaluationError cause: class   
>> org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError
>>
>> Anyone recognize this offhand?
>>
>> Joe

Joseph Kiniry wrote:
> Patrice et al,
>
> On 15 Jul, 2008, at 18:37, Patrice Chalin wrote:
>
>> Can you send the details of one of the tests that is failing?  It 
>> seems that there is a runtime error being raised during the 
>> evaluation of an assertion (recall that definedness checking is now 
>> the default).
>
> After further investigation with both jProfiler and the Eclipse 
> debugger, I'm guessing that the problem is perhaps related to an 
> interaction between the new definedness checking and JML-junit.  I 
> suspect that JML-junit has not being upgraded to support the new 
> default behavior of programs compiled with jmlc, because as far as I 
> recall, there are no jml-junit system tests in JML4.
Right, I do not recall any updates being made to jmlunit.
> Are the old assertion semantics completely gone from JML >= 5.5?  I 
> see no command-line switch to trigger old behavior.
Here is the usage help I get with CVS head:

    usage: org.jmlspecs.jmlrac.Main [option]* [--help] <jml-files>

    Options:
    --Assignable, -A: Check that a method with an assignable clause does
    not call methods that do not have an assignable clause [true]
    --Quiet, -Q: Shuts off all typechecking informational messages [false]
    ...
    * --oldSemantics, -O: use old expression translation mecanism that
    emulates 2-valued logic [false]*

The option you want is --oldSemantics.  I suspect that these should also 
be the options of the 5.5 release.

I'll try to find time to download KOA and try it out though it will 
likely not be before tomorrow (Thursday).

Cheers,
Patrice

-- 
Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof.
Dependable Software Research Group, CSE Department, Concordia University
Room EV3.215, Phone +1-514-848-2424 x3004. http://www.encs.concordia.ca/~chalin

Hi Patrice,

On 16 Jul, 2008, at 13:58, Patrice Chalin wrote:

> Joseph Kiniry wrote:
>>
>> Patrice et al,
>>
>> On 15 Jul, 2008, at 18:37, Patrice Chalin wrote:
>>
>>> Can you send the details of one of the tests that is failing?  It  
>>> seems that there is a runtime error being raised during the  
>>> evaluation of an assertion (recall that definedness checking is  
>>> now the default).
>>
>> After further investigation with both jProfiler and the Eclipse  
>> debugger, I'm guessing that the problem is perhaps related to an  
>> interaction between the new definedness checking and JML-junit.  I  
>> suspect that JML-junit has not being upgraded to support the new  
>> default behavior of programs compiled with jmlc, because as far as  
>> I recall, there are no jml-junit system tests in JML4.
> Right, I do not recall any updates being made to jmlunit.

Ok.

FYI, running our unit tests in JML 5.4 results in error messages that  
make sense, so something changed from 5.4 to 5.5 that is breaking jml- 
junit.

>> Are the old assertion semantics completely gone from JML >= 5.5?  I  
>> see no command-line switch to trigger old behavior.
> Here is the usage help I get with CVS head:
> usage: org.jmlspecs.jmlrac.Main [option]* [--help] <jml-files>
>
> Options:
> --Assignable, -A: Check that a method with an assignable clause does  
> not call methods that do not have an assignable clause [true]
> --Quiet, -Q: Shuts off all typechecking informational messages [false]
> ...
> --oldSemantics, -O: use old expression translation mecanism that  
> emulates 2-valued logic [false] The option you want is -- 
> oldSemantics.  I suspect that these should also be the options of  
> the 5.5 release.

Ah, I was looking at the jml man page, forgetting that jmlc includes  
the extra switches for compilation.

It looks like the new non-null defaults are also biting me, as our  
specs were assuming nullable references.  Unfortunately, as ESC/Java2  
still does not support nullable_by_default, it looks like I'll have to  
update the spec of every reference in the system. :(

For the moment I'll just try to put in nullable_by_default and not use  
ESC/Java2.

> I'll try to find time to download KOA and try it out though it will  
> likely not be before tomorrow (Thursday).

No problem.  I'll perhaps have solved local problems by then, but  
someone should really look at updating jml-junit for the new jmlc  
behavior.

Joe

Hi Joe,
   Can't you revert to nullable by default with jmlc's -n switch?
 --defaultNonNull, -n:                 Make reference paramenters, fields
and method return types non_null by default [true]

    Perry

On Wed, Jul 16, 2008 at 9:18 AM, Joseph Kiniry <kiniry@...> wrote:

>
> It looks like the new non-null defaults are also biting me, as our
> specs were assuming nullable references.  Unfortunately, as ESC/Java2
> still does not support nullable_by_default, it looks like I'll have to
> update the spec of every reference in the system. :(
>
> For the moment I'll just try to put in nullable_by_default and not use
> ESC/Java2.
>

Joseph Kiniry wrote:
> It looks like the new non-null defaults are also biting me, as our 
> specs were assuming nullable references.  Unfortunately, as ESC/Java2 
> still does not support nullable_by_default, it looks like I'll have to 
> update the spec of every reference in the system. :(
>
> For the moment I'll just try to put in nullable_by_default and not use 
> ESC/Java2.
FYI, while I don't plan on implementing support for the 
{non_null,nullable}_by_default modifiers in esc2, I'm almost done with 
adding support for the -nonNullByDefault command line argument (the new 
default works for method return types and parameters).
>> I'll try to find time to download KOA and try it out though it will 
>> likely not be before tomorrow (Thursday).
> No problem.  I'll perhaps have solved local problems by then, but 
> someone should really look at updating jml-junit for the new jmlc 
> behavior.
I agree, though we should try to work towards a jmlunit for jml4.

Cheers,
Patrice

-- 
Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof.
Dependable Software Research Group, CSE Department, Concordia University
Room EV3.215, Phone +1-514-848-2424 x3004. http://www.encs.concordia.ca/~chalin