search

kiniry / Mobius

4 stars 8 forks source link

MIXED vs. PURE refinement checking #627

Open atiti opened 11 years ago

atiti commented 11 years ago

Refinement checking of pure methods does not work reliably. E.g., checking {{{ //@ ensures \result >= 0; public /* pure @*/ int n() { return 0; } }}} against {{{ n: INTEGER ensure Result >= 0; Result /= Void; end }}} results in the warning {{{ TestClass.java:24: n@testpackage.TestClass expected QUERY but found MIXED. bon_skeleton.bon:9: n@TEST_CLASS expected MIXED but found QUERY. 1 Java errors, 0 Java warnings, 0 JML errors and 2 JML warnings found. }}}

atiti commented 11 years ago

From: evka (GH: EvkaD) Date: Sun Jan 31 13:19:33 2010

The error may have resulted from a missing '@', or else the issue has been fixed...