!html

Reply to: noreply@sort.ucd.ie }}} {{{ Bugs item #414, was opened at 2006-08-08 13:00 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=441&aid=414&group_id=97

Category: Semantics Group: None Status: Open Resolution: None Priority: 5 Submitted By: Patrice Chalin (chalin) Assigned to: Nobody (None) Summary: non-pure methods can be used in assertion expressions

Initial Comment: escj allows non-pure methods to be used in assertion expressions. E.g. running escj on

public class NonPure { /@ spec_public / private int i;

//@ ensures \result <==> i > 0;
private boolean m() { return i > 0; }

/*@ private normal_behavior
  @ modifies \nothing;
  @ ensures \result == m();
  @*/
public boolean test() { return !(i <= 0); }

//@ ensures \result <==> i > 0;
public boolean m2() { return i > 0; }

//@ ensures \result == m2();
public boolean test2() { return !(i <= 0); }

}

yields no errors:

ESC/Java version ESCJava-CURRENT-CVS [0.07 s 10339824 bytes] NonPure ... Prover started:0.016 s 12362392 bytes [0.755 s 12543120 bytes] NonPure: m() ... [0.111 s 12031952 bytes] passed NonPure: test() ... [0.033 s 12159784 bytes] passed NonPure: m2() ... [0.021 s 12257504 bytes] passed NonPure: test2() ... [0.023 s 12385128 bytes] passed NonPure: NonPure() ... [0.015 s 12549568 bytes] passed [0.975 s 12550448 bytes total]

yet JMLc rightfully complains:

File "NonPure.java", line 9, character 31 error: A method that is not pure, "m", cannot appear in specification expressions [JML] File "NonPure.java", line 16, character 32 error: A method that is not pure, "m2", cannot appear in specification expressions [JML]

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

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:08:11 2007

added mailto line

This message has 0 attachment(s)

atiti commented 11 years ago

From: None (GH: None) Date: Tue Apr 27 14:34:16 2010

Milestone ESCJava2 2.0.9 release deleted

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:13:59 2007

added mailto line

This message has 0 attachment(s)

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: kiniry (GH: kiniry) Date: Wed Oct 21 12:30:04 2009

Duplicate of #149.

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:18:01 2007

added mailto line

This message has 0 attachment(s)

atiti commented 11 years ago

From: dcochran (GH: dcochran) Date: Thu Jan 10 18:15:44 2008

duplicate of #203

kiniry / Mobius

[ escjava-Bugs-414 ] non-pure methods can be used in assertion expressions #143

!html