search

kiniry / Mobius

4 stars 8 forks source link

feature: non-null by default #155

Open atiti opened 11 years ago

atiti commented 11 years ago

{{{

!html

Reply to: noreply@sort.ucd.ie }}} {{{ Bugs item #580, was opened at 2007-06-26 17:21 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=441&aid=580&group_id=97

Category: Semantics Group: 2.0b1 Status: Open Resolution: None Priority: 5 Submitted By: Gary T. Leavens (leavens) Assigned to: Patrice Chalin (chalin) Summary: Null is still the default for declarations, contrary to JML

Initial Comment: A big, glaring, discrepancy between the current common JML tools (notably the RAC) and ESC/Java2 is the treatment of declarations. In JML, nullable is no longer the default, and you have to explicitly declare something as nullable if it is to permit null. In ESC/Java, I still get these warning about formal parameters, fields, etc. possibly being null. If we're going to have common specification semantics between ESC/Java2 and the other JML tools, this urgently needs fixing.

Comment By: Dermot Cochran (dcochran) Date: 2007-12-15 16:11

Message: These tickets are being transferred into the Mobius Trac

Comment By: Joseph Kiniry (jkiniry) Date: 2007-06-26 23:30

Message: Dunno. Given we just put out a release a few days ago... I'm aiming to release a new version of some Mobius component every week or so, but we are dealing with infrastructure setup at the moment (new machines, new website, new VCS, etc.). Perhaps late July?

Comment By: Patrice Chalin (chalin) Date: 2007-06-26 18:55

Message: What is the ETA for this feature and for the next release of ESC/Java?

Comment By: Joseph Kiniry (jkiniry) Date: 2007-06-26 17:52

Message: Thanks for the nudge Gary.

This feature is planned for the next release of ESC/Java2 & the plugin. For the moment though, we still have a nullable default semantics, as documented.

You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=441&aid=580&group_id=97 }}}

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:14:20 2007

added mailto line

This message has 0 attachment(s)

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Tue Feb 12 13:45:02 2008

This needs to be retested

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Mon Jun 30 11:36:23 2008

Milestone ESCJava2.0b5 release deleted

atiti commented 11 years ago

From: chalin (GH: None) Date: Thu Jul 10 20:17:09 2008

It would be very nice to see this fixed :).

atiti commented 11 years ago

From: chalin (GH: None) Date: Fri Jul 18 23:15:42 2008

Non-null by default (controlled by the command line option -nonNullByDefault) now works for method return types and parameters. Note that the class level modifiers are not supported.

Left to do: Fields and bound variables.

Marked #404 as duplicate.

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Thu Oct 23 17:53:40 2008

Documented in the Implementation Notes