Invocations of Function Objects

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

Short Description

Develop a specification and verification technique for function objects.

This verification problem is directly related to the problem: Specification of methods that use function objects

Code

class Tape {
   public void save(Object o)
   { /* ... */ }
   // other methods omitted
}

class TapeArchive {
   /*@ nullable @*/ Tape tape;
  
   //@ public model boolean isReady;
   //@ represents isReady
   //@                <- tape != null;
   
   //@ ensures isReady;
   public TapeArchive()
   { tape = new Tape(); }
   
   //@ requires isReady;
   public void store(Object o)
   { tape.save(o); }
   
   //@ requires isReady;
   //@ ensures !isReady;
   public void eject()
   { tape = null; }
}

delegate void Archive(Object o);

class Client {
   public static void log(Archive logfile, String s) {
      logfile(s);
   }
}

public class Main {
   public static void main(String[] args) {
      TapeArchive tapeArchive = new TapeArchive();
      Archive archive = new Archive(tapeArchive.store);
      Client.log(archive, "Hello World");
   }
}

A implementation of a tape archive and its client. The represents clause says that the model field isReady is true when a tape is loaded in the archive. The model field provides an implementation-independent specification for the methods of TapeArchive. The delegate Archive provides clients with a uniform way of storing data in different archives.

Specification

Long Description

The code example above shows an implementation of a storage system. The Archive delegate allows one to create function objects for the store methods of different archives. In method Main, the Archive delegate is instantiated with the instance method store. As illustrated by this example, instantiation of a delegate with an instance method also fixes the receiver object of calls to this method, in this case, tapeArchive.
Invoking a function object triggers a call to the underlying method. Verification has to ensure that the requires clause of this method holds when the function object is invoked. Conversely, the properties guaranteed by the underlying method should be available at the invocation site. The challenge is to enable this kind of reasoning.

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