Gary T. Leavens
-
2006-05-18
- assigned_to: cheon --> nobody
According to the preliminary design document, the
predicate \fresh() should check that its arguments are
not null: "\fresh(x,y) asserts that x and y are not null
and that ...". The runtime assertion checker simply
ignores \fresh(), it seems. But it would be better, and
probably simple, to have it check that its arguments are
not null.
An example is in org.jmlspecs.jmlrac.testcase.bugs.Fresh
demonstrates this.