A question on JML - ESC/Java2?component=ESCJava2?type=enhancement

[atiti]

{{{

!html

Reply to: Dermot Cochran }}} {{{ This seems to fit with Gary's suggestion that we should parse-and- ignore any JML keywords which ESC/Java2 does not recognize

Begin forwarded message:

From: Luís Caires Luis.Caires@di.fct.unl.pt Date: February 12, 2008 6:23:59 PM GMT+00:00 To: Mikoláš Janota mikolas.janota@gmail.com Cc: Dermot Cochran Dermot.Cochran@ucd.ie, Joseph Kiniry
kiniry@acm.org, Radu Grigore radugrigore@gmail.com, Joao Costa
Seco Joao.Seco@di.fct.unl.pt Subject: Re: A question on JML - ESC/Java2

Dear Mikolas, Joseph,

Thanks, I know that the crash is inside Simplify :)

My guess is that esc/java is generating garbage for it.

To find the error, you should be able to fully understand what is going on in the VC generator. I guess first-order logic has nothing to do with the crash, trust me ;) Anyway, thanks. If you accept some suggestion: I think that you should rewrite the back-end of the compiler for a well-defined and restricted fragment of JML. No need to cover lots of features if the overall combination gets unusable. Then define a precise semantics for it and manually prove the correctness of the verification condition generator. I do
not really believe in "magic" bugs ;) Perhaps I could chat a bit about this with Joseph at ETAPS, I will be there (have a paper at ESOP).

Thanks,

Luis

PS. Mikolas, the crash has nothing to do with the "recursive" spec it but rather with the
extension to the model function. Of course, to check this you would need to spend some time changing the spec, remove the "recursive spec" of compareTo
from the header files, and play for a while with the tool, systematically
checking what happens. I did it for a couple of weeks before asking for help, but I see
now what might be the source of the problem.

On Feb 12, 2008, at 5:36 PM, Mikoláš Janota wrote:

Hi Luis,

The crashing you see is caused by the prover (Simplify). My guess it that Simplify doesn't handle very well the recursive spec of compareTo.

I believe you can change Simplify's parameters so it doesn't crash, actually it doesn't crash for us here on a linux machine.

Anyhow, the spec has to be loosened. As far as my understanding
goes, such definititions will always cause problems in provers based on the same handling of quantifiers as Simplify.

To summarize: 1) the problem is in the prover, not escjava --- remember that it's first order logic, so there will always be problems 2) the spec is too rigid to be reasonably implemented 3) the spec introduces a problematic expression in the verification condition that is hard to deal with in provers like Simplify

Thank you for your interest!

Best Regards mikolas

On Feb 12, 2008 4:55 PM, Luís Caires Luis.Caires@di.fct.unl.pt
wrote:

== code ==

public class Num implements Comparable {

/_@ specpublic @/ private int n;

Num(int k) { n = k; }

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

/*@ also public normal_behavior

@ ensures \result <==> (\typeof(o) <: \type(Num)); @ public model pure boolean @ definedComparison(non_null Object o) { @ return (o instanceof Num); @ } @*/

//@ also //@ ensures \result == n - ((Num)num).getval(); public int compareTo(Object num) throws ClassCastException { if(num instanceof Comparable) { if(num instanceof Num) { Num m = (Num)num; //@ assert \typeof(m) <: \type(Num); //@ assert \typeof(m) <: \type(Comparable); //@ assert definedComparison(num); //@ assert sgn(n-((Num)num).getval()) == - sgn(((Num) num).getval()-n); return n - m.getval(); } else { //@ assert !definedComparison(num); throw new ClassCastException(); } } else { throw new ClassCastException(); } } }

=== output ==

staff-p3-10:~/JAVA/ESCJava-2.0b4-17-01-08-binary luiscaires$ ./ escjava2 Num.java ESC/Java version ESCJava-2.0b4 [0.058 s 10665208 bytes]

Num ... Prover started:0.038 s 14962600 bytes [0.997 s 14466984 bytes]

Num: Num(int) ... [0.112 s 15135576 bytes] passed

Num: getval() ... [0.035 s 15375792 bytes] passed

Num: definedComparison(java.lang.Object) ...

---

Num.java:16: Warning: Postcondition possibly not established (Post) @ } ^ Associated declaration is "/Users/luiscaires/JAVA/ESCJava-2.0b4-17-01-08-binary/./ escspecs.jar:java/lang/Comparable.spec", line 53, col 12: @ ensures ((\typeof(this) <: \typeof(o)) || ... ^ Execution trace information: Executed return in "Num.java", line 15, col 5.

---

[0.06 s 14879920 bytes]  failed

Num: compareTo(java.lang.Object) ...

---

Num.java:37: Warning: Postcondition possibly not established (Post) } ^ Associated declaration is "/Users/luiscaires/JAVA/ESCJava-2.0b4-17-01-08-binary/./ escspecs.jar:java/lang/Comparable.spec", line 61, col 10: @ ensures sgn(\result) == - sgn(((Comparable)o).compareTo (this ... ^ Execution trace information: Executed then branch in "Num.java", line 22, col 32. Executed then branch in "Num.java", line 23, col 29. Executed return in "Num.java", line 29, col 14.

---

Fatal error: Unexpected exit by Simplify subprocess [1.948 s 16850320 bytes] unexpectedly missing Simplify output [3.152 s 16851104 bytes total] 2 warnings 1 error

On Feb 11, 2008, at 3:42 PM, Mikoláš Janota wrote:

Luis,

could you please provide the example on which it crashes?

thanks, mikolas

On 2/11/08, Luís Caires Luis.Caires@di.fct.unl.pt wrote: Dear Mikolas,

Thanks. Yes, I agree with your analysis. The problem is that we just cannot use the specs as they are, and do not have much time now. About the system crashes I guess it is a bug in the VC
generator. At some point, you should clean up the code, because the system
as it is now seems fairly impredictable... this is particularly serious when we start using it for teaching purposes, maybe you should make it clear in the web site what are the current limitations of the tool. Thanks anyway.

Best regards,

Luis Caires

On Feb 4, 2008, at 2:48 PM, Mikoláš Janota wrote:

Hi Luis,

 you are right that the definedComparison is somewhat odd.

It was apparantly written in the good will that compareTo should be asymmetric, i.e. a.compareTo(b) = -b.compareTo(a) and the each of the side causes an exception if and only if the other one does.

To implement this, one would have to check that the argument of compareTo is a super type of this; and that is something which is difficult to implement in java.

Another problem is that expressing in the postcondition the requirement a.compareTo(b) = -b.compareTo(a) is not a good idea as the reasoning about such specs doesn't really work in escjava, plus it tends to kill the prover.

We will definitely need to rewrite the spec of Comparable.

You said that escjava was crashing when you modified the spec?
Please make sure you have the latest release as I have made some fixes recently, they are not in the plugin yet but should be in the most recent release and of course they are in the svn head.

If it's still crashing, please send us the exact code (or submit a bug report).

Best Regards, mikolas

On Feb 3, 2008 1:16 PM, Luís Caires Luis.Caires@di.fct.unl.pt
wrote: 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

Mikoláš Janota M. Sc. School of Computer Science and Informatics, University College Dublin, Belfield, Dublin 4, Ireland

Mikoláš Janota M. Sc. School of Computer Science and Informatics, University College Dublin, Belfield, Dublin 4, Ireland

Mikoláš Janota M. Sc. School of Computer Science and Informatics, University College Dublin, Belfield, Dublin 4, Ireland

Dermot Cochran Dermot.Cochran@ucd.ie Systems Research Group School of Computer Science & Informatics UCD CASL 8 Belfield Office Park Clonskeagh Dublin 4, Ireland Tel: +353-1-716-5349

}}}

[atiti]

From: Dermot Cochran (GH: None) Date: Wed Feb 13 09:47:57 2008

added mailto line

This message has 1 attachment(s)