#72 JML checker doesn't say what methods must be overridden

[Riccardo Casero]

Let's take this example. I think everything is fine but I
don't understand why:

1) jml and jmlc are not complaining about the due
overriding of Add(Object o) in MyCountedSet. Since
there's a new variable which depends on objects
(cardinality is in its data group) it must be updated
everytime objects is assignable, mustn't it?

2)when I execute Sets.Main no excetption is thrown
even if cardinality!=objects.size()

Thanx in advance -Riccardo-

------------------------------------------------

MySet.jml

package Sets

//@model import org.jmlspecs.models.*;

public class MySet{

//@public model JMLObjectSet objects;

//@public invariant objects!=null;

//@public normal_behavior
//@ assignable objects;
//@ ensures o!=null ==> objects.has(o);
public void Add(Object o);

//@public normal_behavior
//@ assignable objects;
//@ ensures s!=null ==> (\forall Object o;s.objects.has
(o);objects.has(o));
public void AddAll(MySet s);

}

------------------------------------------------
MySet.java

package Sets;

//@refine "MySet.jml";

import java.util.HashSet;
import java.util.Iterator;

//@ model import org.jmlspecs.models.*;

public class MySet{

protected HashSet hidden_representation;
//@ in objects;
//@ maps
hidden_representation.theSet \into objects;

//@protected represents objects <-
JMLObjectSet.convertFrom(hidden_representation);

public void Add(Object o){
hidden_representation.add(o);
}

public void AddAll(MySet s){
Iterator iter=s.hidden_representation.iterator();
for(;iter.hasNext();){
Add(iter.next());
}
}

public MySet(){
hidden_representation=new HashSet();
}
}

------------------------------------------------------

MyCountedSet.java

package Sets;

public class MyCountedSet extends MySet{

//@ public model int cardinality;
//@ in objects;

protected int number_of_elements;
//@ in cardinality;

//@ protected represents cardinality <-
number_of_elements;
//@ public represents objects \such_that
cardinality==objects.size();

//@ public normal_behavior
//@ ensures \result==cardinality;
public /*@ pure @*/ int cardinality(){
return number_of_elements;
}

}

------------------------------------------------------
--

package Sets;

public class Main{

public static void main(String[] args) throws
java.io.IOException{
MyCountedSet mcs=new MyCountedSet();
System.out.println("Cardinality:"+mcs.cardinality());
System.out.println("Adding a new object to a newly
created MyCountedSet");
mcs.Add(new Object());
System.out.println("Done!");
System.out.println("Cardinality:"+mcs.cardinality());
System.in.read();
}

}

------------------------------------------------------
----

[Gary T. Leavens]

Logged In: YES
user_id=633675

Hi Ricardo,

Problem 1 occurs because JML's support for checking
assignable clauses doesn't yet deal with maps \into. That is
it doesn't handle dynamic dependencies. We plan to do that,
but it will take a while.

Problem 2 happens because I don't think the runtime
assertion checker deals with the \such_that form of
represents clauses yet. You could use an invariant instead,
and it would give an error on this example, I think.

I'm chaning this to a feature request. Thanks for the nice
examples.

[Riccardo Casero]

Logged In: YES
user_id=907623

I'm not sure I understand your request. Can you provide more
information and/or an example?

[Riccardo Casero]

Logged In: YES
user_id=907623

Thanks for your quick answer! Regarding problem2 you're
right: if I state the same condition in an invariant like

//@ public invariant objects.size()==cardinality;

in MyCountedSet.java I get an exception.

But regarding the first problem I don't think it's a matter of
dynamic dependencies. In fact take this simplified version of
the same problem:

-------------------------------------
package Test;

public class Number {
//@public model double number;

protected double n;
//@ in number;

//@ represents number <- n;

/*@ public normal_behavior
@ ensures number==x;
@ assignable number; @*/
public Number(double x){
n=x;
}

/*@ public normal_behavior
@ ensures number==(2*\old(number));
@ assignable number; @*/
public void Double(){
n=2*n;
}

/*@ public normal_behavior
@ ensures \result == number; @*/
public /*@ pure @*/ double Value(){
return n;
}

public void method1(){
}

public void method2(){
method1();
}

}

------------------------------------------

package Test;

public class Number2 extends Number{

protected /*@ spec_public @*/ double double_n;
//@ in number;

//@protected represents number <- (double_n/2);

/*@ public normal_behavior
@ ensures number==x;
@ assignable number; @*/
public Number2(double x){
super(x);
double_n=2*n;
}

public void method1(){
method2();
}

}

-----------------------------------------

In this case there's no dynamic dependence. Still when I
jmlcompile Number2.java the fact that I should override Double
() in order to make it update the value of double_n is not
signalled. What I'm trying to understand is whether jml is
checking that Double() override in Number2 has "additional
side effects" or not.

In addition in this example I put the method1() and method2
() methods to force a callback cycle, but it went undetected.

Thanks -Riccardo-

[Gary T. Leavens]

Logged In: YES
user_id=633675

You are right that JML does not yet enforce the rules the
Clyde Ruby and I wrote about in OOPSLA 2000 for what
methods must be overridden in subclasses. Clyde Ruby
hasn't implemented tools to complain about what methods
should be overriden yet, although he's working on that.

So JML's current static analysis isn't going to detect that
Double should be overridden in Number2. But you do get a
runtime assertion failure if you call Double on a Number2
object in this latest example. The postcondition of Double
doesn't hold.