Comparable specification in JML and ESC/Java2

[atiti]

{{{

!html

Reply to: Dermot Cochran }}} {{{

Begin forwarded message:

From: Luís Caires Luis.Caires@di.fct.unl.pt Date: 3 February 2008 13:16:23 GMT To: Dermot Cochran Dermot.Cochran@ucd.ie Cc: Joseph Kiniry kiniry@acm.org, Radu Grigore
radugrigore@gmail.com, Mikolas Janota mikolas.janota@gmail.com,
Joao Costa Seco Joao.Seco@di.fct.unl.pt Subject: Re: A question on JML - ESC/Java2

Hi,

Thanks for your email.

Well, as far as we can tell, model methods are being checked as any other method, if you provide an "implementation". In any case, the verifier relies on the spec as usual.

A problem is that the spec of definedComparison is very funny. It bugs me that such a key spec seems to never have been checked ;) If we try to refine it, e.g., so that it would express the correct type constraints, the compiler crashes. In fact, it crashes if one attempts to refine definedComparison by adding trivial constraints. How should we fix that? It would be easy to rewrite the spec ... and we wouldn't need to call for a support request to do that.

There are also lots of issues with frame condition specs. The fact is that presently, we are not being able to show to the students how to check much more than simple Pascal-like algorithms, inside a single
class, with esc/java2. Maybe this is because of the lack of documentation, but i am not sure about that. Is there some specification about how "modifies" clauses are being formally handled in the underlying
logic ? How are frame conditions handled? I am bugged that in the examples only single classes are ever handled... Do you have an example where calling a non pure method of an external object does not break the current proof state? Where should we look for the semantics of the assertion language ? Thanks,

Best, Luis

On Feb 1, 2008, at 10:22 PM, Dermot Cochran wrote:

The others can confirm/deny this; but it looks as if model methods
are not fully checked by ESC/Java2, so that definedComparison is
assumed to be true and the exceptional behavior is unexpected.

On 1 Feb 2008, at 18:38, Joseph Kiniry wrote:

Hello Luis,

I'm sorry I have not yet had time to look at your question.
Perhaps you can submit a support request at the Mobius Trac?
(http://mobius.ucd.ie/) Also, perhaps one of my group (CCed) can
help you out quicker than I can.

Thanks for your interest, Joe

On 30 Jan, 2008, at 19:24, Luís Caires wrote:

Dear Joseph,

We intended to write to the jmlspecs-escjava mailing list, but perhaps it would be faster to check this directly with you (or maybe you may just fwd this to some of your collaborators). We are trying to use esc/java2 in some non-trivial examples in a MSc course, but in fact are finding difficulties in some quite trivial examples...

For example, why does the following code fails to go through the esc/java2 compiler (last version)?

Is there any test case for the comparable interface that works ok? We have been struggling with this for quite a while.

Thanks in advance,

Luis Caires http://ctp.di.fct.unl.pt/~lcaires/

=====>

public class Num implements Comparable {

private int n;

Num(int k) { n = k; }

//@ ensures \result == n; /@ pure @/ public int getval() { return n; }

public int compareTo(Object num) {

  if(num instanceof Num) {
          Num m = (Num)num;
          return m.getval() - this.n;
  } else
      throw new ClassCastException();

} } =====>

Begin forwarded message:

From: "Gary T. Leavens" leavens@eecs.ucf.edu Date: January 30, 2008 3:51:32 PM GMT+00:00 To: Luís Caires luis.caires@di.fct.unl.pt Cc: Joao Costa Seco Joao.Seco@di.fct.unl.pt Subject: Re: A question on JML - ESC/Java2

Hi Luis,

I see that an example that works with ESC/Java2 is what you
need, but I'm not working enough with that tool to help. Please post your request to the jmlspecs-escjava mailing list and I'm sure someone there can find a good example for you.

On Tue, 29 Jan 2008, [ISO-8859-1] Luís Caires wrote:

Hi Gary,

thanks for your time.

On Jan 29, 2008, at 3:14 AM, Gary T. Leavens wrote:

Hi Luis, On Mon, 28 Jan 2008, [ISO-8859-1] Luís Caires wrote:

We are doing some experimentation with ESC/Java2 in a MSc
course on software construction, in particular trying to understand
some of the specs for the Java framework. I am a bit puzzled by your spec of
compareTo in Comparable. (For the record, let me say that it was the "et al." that
wrote that specification. The one I wrote in the Common JML tools is
considerably less constructive.) In definedComparision, how can we assure that either \typeof(this) <: \typeof(o) or typeof(o) <: \typeof(this)? We can't in general. But we don't have to. The ensures
postcondition (\typeof(this) <: \typeof(o)) || (\typeof(o) <: \typeof(this))) ==> \result; says only that if either \typeof(this) <: \typeof(o) or typeof(o) <: \typeof(this) , then \result must be true. If the hypothesis of this implication is false, then this postcondition is trivially satisfied (since false ==> \result is always true).

Yes, clearly the assertions hold as you say, I was rather asking what is the intent of such a postcondition spec, that will always be trivially true most of the time without saying much about \result.

we also see that definedComparision is expected to be refined in subclasses, but unfortunately ESC/Java2 crashes when we try to do that :).

In general we only have both typeof(o) <: \typeof(K) and typeof(this) <:
\typeof(K) for some subtype K of Comparable, right? Well, we know \typeof(this) <: \typeof(Comparable) since this
is a specification in type Comparable. So the second part is
trivially true. The first part must be true due to the precondition in
the specification case in question.

Oh, not really, since the precondition need not mention types
at all.

It would be a time saver to be able to look at some example that works :) Well, I already browsed the whole web for an example of use of the Comparable spec in ESC/Java2 and I did not find any. Nice to deal with such complex specs, but it turns
out a bit unfortunate that we cannot easily check them with some tool. In any case, this is certainly a very promising and impressing
work direction.

Thanks for point to the mailing list, let's see.

Thanks,

Luis http://ctp.di.fct.unl.pt/~lcaires/

Best regards, Luis http://ctp.di.fct.unl.pt/~lcaires/ PS1: /\ JML's specification of java.lang.Comparable.

• These are objects with a total ordering that is an
  equivalence relation.
• @version $Revision: 2240 $
• @author Gary T. Leavens, et al. / /@ public normal_behavior @ requires !(\typeof(o) <: \type(Comparable)); @ ensures !\result; @ also public normal_behavior @ requires \typeof(o) <: \type(Comparable); @ ensures ((\typeof(this) <: \typeof(o)) || @ (\typeof(o) <: \typeof(this))) ==> \result; @ // subclasses will strengthen this contract. @ public model pure boolean @ definedComparison(nonnull Object o); @/ /_@ public exceptional_behavior @ requires !definedComparison(o); @ signals_only ClassCastException; @ also public normalbehavior @ requires definedComparison(o); @ ensures (o == this) ==> \result == 0; // reflexive @ ensures sgn(\result) == - sgn(((Comparable) o).compareTo(this)); // antisymmetric @/ /@ pure @/ int compareTo(/_@ nonnull / Object o); PS2: public class Num implements Comparable { private int n; Num(int k) { n = k; } //@ ensures \result == n; /@ pure @/ public int getval() { return n; } public int compareTo(Object num) throws ClassCastException { if(num instanceof Num) { /_@ non_null @*/ Num m = (Num)num; return m.getval() - this.n; } else throw new ClassCastException(); } } Gary T. Leavens 210 Harris Center (Bldg. 116) School of EECS, University of Central Florida 4000 Central Florida Blvd., Orlando, FL 32816-2362 USA http://www.eecs.ucf.edu/~leavens phone: +1-407-823-4758 leavens@eecs.ucf.edu

    Gary T. Leavens
    210 Harris Center (Bldg. 116)
    School of EECS, University of Central Florida
    4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
    http://www.eecs.ucf.edu/~leavens  phone: +1-407-823-4758
    leavens@eecs.ucf.edu

---

Dr. Joseph Kiniry http://casl.ucd.ie/people/ kiniry KindSoftware Research Group http:// kind.ucd.ie/ Systems Research Group http:// srg.cs.ucd.ie/ UCD School of Computer Science and Informatics http://www.ucd.ie/ csi/ Complex & Adaptive Systems Laboratory (UCD CASL) http:// casl.ucd.ie/ University College Dublin http:// www.ucd.ie/ Belfield, Dublin 4, Ireland

}}}

[atiti]

From: Dermot Cochran (GH: None) Date: Sun Feb 3 20:34:58 2008

added mailto line

This message has 1 attachment(s)

[atiti]

From: dcochran (GH: dcochran) Date: Mon Feb 4 13:02:48 2008

This example seems to crash the ESC/Java2 plugin...

[atiti]

From: dcochran (GH: dcochran) Date: Mon Jun 30 11:36:23 2008

Milestone ESCJava2.0b5 release deleted

[atiti]

From: kiniry (GH: kiniry) Date: Tue Aug 25 15:47:07 2009

Duplicate of #458.

[atiti]

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

Milestone ESCJava2 2.0.9 release deleted