Status: Closed
Resolution: Out of Date
Priority: 3
Submitted By: Joseph Kiniry (jkiniry)
Assigned to: Robin Green (greenrd)
Summary: immutability
Initial Comment:
Several papers have been written proposing adding a const-like keyword, typically called "immutable" to JML. The most recent and advanced of these proposals are by Michael Ernst (see his work on the Javari system) and Erik Poll (see his talk and draft paper about immutability).
Checking that a class has properly implemented immutability is very difficult in the general case. Erik's proposal constrains the manner in which one can safely implement immutability in Java to such a degree that checking is straightforward. We hope that his proposal is not overly constrained wrt developer's needs as well, but we will not know such until we have an implementation with which we can experiment.
Checking with immutable objects/classes, on the other hand, is quite easy and useful.
The purpose of this project is to add support for immutability to ESC/Java2. This would entail understanding the existing proposals and realising them in one or more of the logics in which we reason and modifying the parser and VC generator(s) appropriately.
Initial researchers: Robin Green, Joe Kiniry, Erik Poll, Michael Ernst
{{{
!html
Reply to: noreply@sort.ucd.ie }}} {{{ Research item #196, was opened at 2005-10-26 12:23 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=780&aid=196&group_id=97
Category: None Group: None
Initial Comment: Several papers have been written proposing adding a const-like keyword, typically called "immutable" to JML. The most recent and advanced of these proposals are by Michael Ernst (see his work on the Javari system) and Erik Poll (see his talk and draft paper about immutability).
Checking that a class has properly implemented immutability is very difficult in the general case. Erik's proposal constrains the manner in which one can safely implement immutability in Java to such a degree that checking is straightforward. We hope that his proposal is not overly constrained wrt developer's needs as well, but we will not know such until we have an implementation with which we can experiment.
Checking with immutable objects/classes, on the other hand, is quite easy and useful.
The purpose of this project is to add support for immutability to ESC/Java2. This would entail understanding the existing proposals and realising them in one or more of the logics in which we reason and modifying the parser and VC generator(s) appropriately.
Initial researchers: Robin Green, Joe Kiniry, Erik Poll, Michael Ernst
You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=780&aid=196&group_id=97 }}}