jml-unit, and esc/java2 with non-null by default

[Gary T. Leavens-2]

Hi Patrice, Joe,

On Wed, 16 Jul 2008, Patrice Chalin wrote:

> 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 would be great if ESC/JavaN were more compatible, especially the
-nonNullByDefault command line argument.  I had various problems with
that during tutorials last year.

>>> 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.

I agree we should have a jmlunit that works with jml4.

However, I'm not sure I understand why the JML2 jmlunit is broken with
JML 5.5 still.  Our unit tests for jmlunit are passing, so what are we missing?

         Gary T. Leavens
         210 Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Joseph Kiniry]

Hi Gary,

On 16 Jul, 2008, at 15:23, Gary T. Leavens wrote:

> Hi Patrice, Joe,
>
> On Wed, 16 Jul 2008, Patrice Chalin wrote:
>
>> 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 would be great if ESC/JavaN were more compatible, especially the
> -nonNullByDefault command line argument.  I had various problems with
> that during tutorials last year.

Looks like Patrice just committed the final (?) change to enable this  
switch for 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.
>> I agree, though we should try to work towards a jmlunit for jml4.
>
> I agree we should have a jmlunit that works with jml4.

Dan Zimmerman and I are working along this front now, though it isn't  
clear whether we will augment JML2's jmlunit initially or build  
something new in JML4.

> However, I'm not sure I understand why the JML2 jmlunit is broken with
> JML 5.5 still.  Our unit tests for jmlunit are passing, so what are  
> we missing?

I don't know.  I'll work on attempting to use the new semantics with  
non-null defaults in 5.5 and see where I get.

Joe


-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Patrice Chalin-3]

Joseph Kiniry wrote:
> Hi Gary,
>
> [snip]
> Looks like Patrice just committed the final (?) change to enable this
> switch for ESC/Java2.
No. Still need to add support for default nullity of fields and bound
variables (e.g. inside quantifiers). That should happen later this week.
Of course, ESC4 is already supporting the proper behavior w.r.t. nullity
and defaults.
> Dan Zimmerman and I are working along this front now, though it isn't
> clear whether we will augment JML2's jmlunit initially or build
> something new in JML4.
Nice!
>> However, I'm not sure I understand why the JML2 jmlunit is broken with
>> JML 5.5 still.  Our unit tests for jmlunit are passing, so what are
>> we missing?
> I don't know.  I'll work on attempting to use the new semantics with
> non-null defaults in 5.5 and see where I get.
Ok.

Cheers,
Patrice

--
Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof.
Dependable Software Research Group, CSE Department, Concordia University
Room EV3.215, Phone [phone] x3004. www.encs.concordia.ca/~chalin


-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Gary T. Leavens-2]

HI Joe,

On Wed, 16 Jul 2008, Joseph Kiniry wrote:

> On 16 Jul, 2008, at 15:23, Gary T. Leavens wrote:
>
>>>>> 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.
>>
>> I agree we should have a jmlunit that works with jml4.
>
> Dan Zimmerman and I are working along this front now, though it isn't clear
> whether we will augment JML2's jmlunit initially or build something new in
> JML4.

That sounds good, I'm glad to hear it.

>> However, I'm not sure I understand why the JML2 jmlunit is broken with
>> JML 5.5 still.  Our unit tests for jmlunit are passing, so what are we
>> missing?
>
> I don't know.  I'll work on attempting to use the new semantics with non-null
> defaults in 5.5 and see where I get.

Ok, keep us informed...

         Gary T. Leavens
         210 Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers