specifying static initialization

[davidcok]

Consider

class A {
   final static int a = B.b;
}

The value that A.a is initialized with may depend on whether B has not yet started initialization, has started but not yet finished, or has completed initialization. Dependency loops can result in initialized values that depend on the order of initialization.

I don't aim for JML to be able to specify and verify cases where there are mutually dependent static initialization behaviors. But it would be good to be able to write specs that exclude them. For that the \isInitialized(T) predicate is insufficient (it is true when initialization is complete). What is needed is a predicate that states "not being initialized" or equivalently "either not started initialization or already completed initialization". Perhaps \isInitializing(T) for the former?

Here is a more detailed use case.

public class A extends B {
  final static int a = B.b;
  static int aa = 42;
  public static void main(String... args) { System.out.println("A.main: " + A.a + " " + A.aa + " " + B.b); }
}
public class B {
  final static int b = A.aa;
  public static void main(String... args) { System.out.println("B.main:" + A.a + " " + A.aa + " " + B.b);}
}

If you run A.main you get: A.main: 0 42 0 If you run B.main you get: B.main:0 42 42

To catch the circular dependency, one could put /*@ requires !\isInitializing(A); static_initializer */in B or /*@ requires !\isInitializing(B); static_initializer */ in A. With this one can modularly detect circular dependencies (I think)

[mattulbrich]

Actually, KeY claims that it correctly models static initialisation - if it is switched on. It is hardly ever switched on. The overhead is enormous. A simple new B() in becomes where the @(<xyz>) refers to the static synthetic verification-only field xyz (I think).

[davidcok]

Do you have a modular solution without additional specifications? I can certainly see that dependency-loops can be detected with a whole program analysis, but that is not in the JML spirit. I can also see that the relevant specifications could be inferred, at last in many cases. It would be a bit more complex if initialization uses some static methods.

[leavens]

I'm not sure that there is a modular solution for static initialization, as it is not very modular in Java itself. Maybe the best methodology is to avoid any effects during static initialization, so that static initialization happening at unpredictable times will not cause verifications to become invalid. It's an interesting research topic.