Java Modeling Language (JML) / Feature Requests / #67 Enforce purity declarations in checker

#67 Enforce purity declarations in checker

Status: open

Owner: Cui

Labels: checker (i.e., the jml tool) (25)

Module:

Priority: 6

Updated: 2013-10-27

Created: 2003-10-21

Creator: Gary T. Leavens

Private: No

This is partly implemented, but dynamic dependencies
on handled and there are still some loopholes.

Discussion

Gary T. Leavens - 2003-10-21

assigned_to: cheon --> nobody
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Gary T. Leavens - 2006-05-18

priority: 5 --> 6

assigned_to: nobody --> ye-cui
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Gary T. Leavens - 2006-05-18

Logged In: YES
user_id=633675

Cui, this also falls into the assignable clause checking area.
If you can implement it, that would be great.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Gary T. Leavens - 2006-10-01

Logged In: YES
user_id=633675

David Shaw also reported this problem in terms of not
checking dynamic dependencies.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Log in to post a comment.