[ escjava-Bugs-270 ] method call resolution (static vs. dynamic types)

[atiti]

{{{

!html

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

Category: VC Generation Group: CVS HEAD Status: Open Resolution: None Priority: 2 Submitted By: Joseph Kiniry (jkiniry) Assigned to: Radu Grigore (rgrig) Summary: method call resolution (static vs. dynamic types)

Initial Comment: Martijn Warnier reported a bug in method call type resolution back in April of 2005 and it was never filed. Here is the email exchange with David Cok on the matter.

---

From:     warnier@cs.vu.nl
Subject:    Fwd: Desugaring Bug in ESC/Java2?
Date:   22 April, 2006 23:05:35 GMT+02:00
To:       kiniry@acm.org

Hey Joe,

here's my original bug-report (including David Cok's response) about the late vs early binding stuff we discussed today.

Martijn

Begin forwarded message:

From: David Cok cok@frontiernet.net Date: Thu 14 Apr 2005 23:12:33 GMT+02:00 To: Martijn Warnier warnier@cs.ru.nl Cc: Joe Kiniry kiniry@acm.org Subject: Re: Desugaring Bug in ESC/Java2? Reply-To: cok@frontiernet.net

Martijn,

Thanks for the report.

1) When ESC/Java2 prints out the "Desugared specs" it does not include those it inherits. Those are combined later on. Since the super class desugared specs are also printed out, typically, the information is there. But the "desugared specs" don't precisely match what Gary's desugaring paper would say (for other reasons as well).

2) ESC/Java2 currently uses the specs of the static type of the receiver when reasoning about a method call. This is what causes the Error in each of the cases you highlight. The receiver in each case is p2, which is statically typed as Point, though its dynamic type is ColorPoint. I have a means of fixing this, but it is not in that alpha release. So this behavior is not unexpected to me.

Note two things: a) If you put in a cast as in r3 = ((ColorPoint)p2).equals(p1); //@ assert r3 == 2; //ESC/Java2 gives a warning here. the warning goes away, because the static type is now ColorPoint.

b) It is not the case the escjava thinks that r3 is 1 - you would get a possible assertion failure in that case as well, e.g. r4 = p2.equals(p2); //@ assert r4 == 1; //ESC/Java2 gives a warning here. It can deduce that p2 has dynamic type ColorPoint for the purpose of evaluating \typeof, but it does not yet bring in the specs of ColorPoint at the point of call as assumptions.

• David

Martijn Warnier wrote:

Hi Joe and David,

As I already mentioned at ETAPS, I've been playing with ESC/Java2 recently. I think I found a desugaring bug. Consider the following example:

\ EXAMPLE **

class Point{

 /*@ normal_behavior
   @  requires true;
   @ assignable \nothing;
   @ ensures  (\typeof(this) == \type(Point)) ==> \result == 1;
   @*/
 int equals(Point x){return 1;}

}

class ColorPoint extends Point{

 /*@ also
   @ normal_behavior
   @  requires \typeof(this) == \type(ColorPoint);
   @ assignable \nothing;
   @ ensures  \result == 2;
   @*/
int equals(Point x){return 2;}

}

class Inheritance{

  public int r1,r2,r3,r4,r5,r6,r7,r8,r9;

  /*@ normal_behavior
    @  requires true;
    @   assignable r1,r2,r3,r4,r5,r6,r7,r8,r9;
    @  ensures  true;
    @*/
  void m(){
    Point p1 = new Point();
    Point p2 = new ColorPoint();
    ColorPoint cp = new ColorPoint();
    r1 = p1.equals(p1);
    //@ assert r1 == 1;
    r2 = p1.equals(p2);
    //@ assert r2 == 1;
    r3 = p2.equals(p1);
    //@ assert r3 == 2;  //ESC/Java2 gives a warning here.
    r4 = p2.equals(p2);
    //@ assert r4 == 2;  //ESC/Java2 gives a warning here.
    r5 = cp.equals(p1);
    //@ assert r5 == 2;
    r6 = cp.equals(p2);
    //@ assert r6 == 2;
    r7 = p1.equals(cp);
    //@ assert r7 == 1;
    r8 = p2.equals(cp);
    //@ assert r8 == 2;  //ESC/Java2 gives a warning here.
    r9 = cp.equals(cp);
    //@ assert r9 == 2;
  }

}

** END EXAMPLE *

ESC/Java2 gives warnings at three points where it shoudn't warn. I looked at the desugaring of both equals specs. and found that the equals in class ColorPoint is desugared as:

Desugared specifications for ColorPoint.equals requires (\lblneg Pre:0.15.9 this instanceof ColorPoint && \typeof(this) == \type(ColorPoint)) signals (java.lang.Exception)\old(this instanceof ColorPoint && \typeof(this) == \type(ColorPoint)) ==> false /@ modifies \old(this instanceof ColorPoint && \typeof(this) == \type(ColorPoint)) ==> (\nothing); @/ ensures \old(this instanceof ColorPoint && \typeof(this) == \type(ColorPoint)) ==> \result == 2 diverges \old(this instanceof ColorPoint && \typeof(this) == \type(ColorPoint)) ==> false Desugaring specifications for ColorPoint.ColorPoint --- parsed specs --- /@ @/

Shouldn't this method inherit the spec form the equals method in class Point (as indicated by the JML keyword also) ? I used the latest binary release of ESC/Java2 (a8). Please let me know if you know what the problem is here.

best,

Martijn

---

Comment By: David Cok (davidcok) Date: 2006-10-20 23:04

Message: This is a duplicate of #269 (so #269 was closed). This comment is copied from there:

ESC/Java and ESC/Java2 (and I think jmlc) use the specifications of the static type at the point of a method call. So in the r3 situation, p2 has static type Point, so the specs of Point and its superclasses are utilized in forming the VC. The specs of any derived classes are not. Usually derived classes are not even visible, though in this example ColorPoint is.

I have noted this issue before (even in some publication I think). It would be a design change, that perhaps we should consider, to add in the specs of any overriding methods that are visible as well.

---

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

[atiti]

From: (GH: None) Date: Sat Dec 15 17:07:50 2007

added mailto line

This message has 0 attachment(s)

[atiti]

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

Milestone ESCJava2 2.0.9 release deleted

[atiti]

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

added mailto line

This message has 0 attachment(s)

[atiti]

From: dcochran (GH: dcochran) Date: Fri Jan 11 15:29:11 2008

Duplicate of #240

[atiti]

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

added mailto line

This message has 0 attachment(s)

[atiti]

From: kiniry (GH: kiniry) Date: Wed Oct 21 12:27:55 2009

Duplicate of #142.