Modification of Static Fields

June 22, 2010 – 6 years, 9 months ago, by eifler

Short Description

Develop a specification and verification technique that allows one to determine the effects of methods on static fields.

Code

import java.util.Date;
public abstract class Operation {
   //@ public model JMLDataGroup runGroup;
   
   private /*@ spec_public @*/ static long operations;
   private /*@ spec_public @*/ static long elapsedTime;
   private static Date date = new Date();
   
   //@ public static invariant 0 <= operations;
   
   //@ assignable runGroup;
   protected abstract void run();

   //@ assignable operations, elapsedTime, runGroup;
   public void perform() {
      long start = now();
      run();
      operations++;
      elapsedTime += now() - start;
      long avg = elapsedTime / operations;
      System.out.println(avg);
   }

   //@ assignable operations, elapsedTime;
   //@ ensures operations == 0 && elapsedTime == 0;
   public static void reset() {
      operations = 0;
      elapsedTime = 0;
   }
   
   protected long now() {
      return date.getTime();
   }
}

A Java class with some static fields. In this example, the correctness of method perform relies on the fact that executions of now do not change the value of operations. The field runGroup is a model field, and hence only usable in specifications. The type JMLDataGroup is used in such declarations to declare data groups

Specification

Long Description

Most of the state of an object-oriented program resides in the fields of objects, but there are also situations where some state is shared among all instances of a class. In those situations, one can use global variables, or static fields as Java and C# call them. A problem arises in reasoning about when static fields change.
The program above declares an abstract class whose overridable run method performs an operation of some sort. The public method perform invokes run, bracketing the invocation with calls to now, which retrieves the current time. The class keeps track of the number of operations that have completed since the counters of the class were last reset, and also keeps track of the sum of the times elapsed during those operations. Method perform ends by computing and printing the average time elapsed during an operation.
The correctness of the implementation of perform depends on operations being non-zero at the time the average is computed, thus avoiding a division-by-zero error. The class invariant states that operations is at least zero, so the increment will make operations positive. The implementation of perform is therefore correct, provided the second call to now has no effect on the static field operations, more specifically that it does not set it to zero. Such an undesired effect could, for instance, occur if an override of now in a subclass of Operation would call reset. This shows that method specifications must express which static fields are potentially modified by the method.
The effect of a method on instance fields is described by the method’s assignable clause. However, stipulating that a method also affects only those static fields listed in the method’s assignable clause has a couple of fatal flaws. First, the discipline violates information hiding, because public methods would have to advertise any private static fields that they modify. Second, the assignable clause of a method would become overly verbose, because it would have to include all static fields modified by all transitive callees. The need to declare modifications of both private static fields and static fields modified by transitive callees in assignable clauses is due to potential reentrancy. Consider for instance a method C.caller that calls D.middle, which in turn calls C.callee. If C.callee modifies a private static field of class C, then this modification has to be advertised to C.caller and, therefore, must be declared in the assignable clauses of both C.callee and D.middle. Dealing with the information hiding problem and the transitivity problem is an open challenge.

Supplementary Materials

The paper by Gary T. Leavens and K. Rustan M. Leino and Peter Müller from which this challenge is taken contains some additional information including references to relevant papers related to this challenge. Some more specification and verification challenges which are also included on this site can also be found there.

Submitted by

Timo Eifler verifythis@cost-ic0701.org