!html

Reply to: noreply@sort.ucd.ie }}} {{{ Bugs item #111, was opened at 2005-07-21 11:59 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=441&aid=111&group_id=97

Category: VC Generation Group: CVS HEAD

Status: Closed Resolution: Out of Date Priority: 2 Submitted By: Joseph Kiniry (jkiniry) Assigned to: Alan Morkan (alanm) Summary: Recursive postconditions

Initial Comment: If a pure method mentions itself in a postcondition it looks like things blow up due to the recursion.

Comment By: Dermot Cochran (dcochran) Date: 2007-12-15 16:16

Message: These tickets are being transferred into the Mobius Trac

Comment By: Dermot Cochran (dcochran) Date: 2007-05-11 16:16

Comment By: Clement Hurlin (smelc) Date: 2007-05-11 13:03

Message: As Joe's previous post said, JML provides keyword measured_by to make explicit the argument of well-foundness, as in this example:

class Node{ int x; Node next;
//@ invariant (next != null) ==> next.x < this.x;

//@ measured_by(this.x);
//@ ensures (next != null) ==> (\result == x * next.multiply());
//@ ensures (next == null) ==> (\result == x);
/*@ pure @*/ int multiply(){
if(next == null) 
    return x;
else 
    return x * next.multiply(); 
}

}

However, escjava2 fails to parse this example with the following message: "Node.java:4: Error: This clause may only be in a code_contract section //@ measured_by(this.x); ^"

This looks like something is implemented for that in escjava2 but JML's syntax has changed since: the code_contract keyword mentionned in the error message is deprecated because code_contract has been removed from JML (cf Section 20.2 of JML's Manual)

Comment By: Joseph Kiniry (jkiniry) Date: 2005-10-24 11:18

Message: I am assigning this to Alan. Alan, please read the paper in question and we'll all need to think about how to detect these situations properly to improve our soundness and robustness. Make sure to chat with Radu and Robin about it as well so lots of grey matter gets applied to the problem.

Comment By: Joseph Kiniry (jkiniry) Date: 2005-08-20 16:20

Message: Recursive specifications are discussed in Davas and Muller's FTfJP05 paper, section 6.2. They note that this can lead to unsoundness. The example they use is:

class Cycle { /_@ normalbehavior @ ensures \result == direct() + 1; @/ /@ pure @/ int direct() { return 5; } }

They completely forbid recursive specifications at this time. They say that this can be checked by checking that the call graph of a program, including all specifications, rooted at a given pure method use in an assertion, is non-cyclic.

They say that, while recursive specs are usually an indication that a spec is redundant or flawed, completely forbidding them is too restrictive. E.g., factorial and equals methods of are specified recursively. They claim that for their axiomisation, it is sufficient to prove that such a recursive specification is "well-founded", but they do not state what that means.

They say that investigating the different means of guaranteeing weel-foundedness is future work. They plan on using some combination of measured_by and Universes.

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

atiti commented 11 years ago

From: (GH: None) Date: Sat Dec 15 17:19:59 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

kiniry / Mobius

[ escjava-Bugs-111 ] Recursive postconditions #176

!html