Methods that Use Function Objects

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

Short Description

Develop a specification technique for methods that use function objects.

Code

Example Code 1

class Paragraph {
   char[][] text;
   int width;
   
   //@ assignable text;
   public void format(Formatter f) {
      f(this);
   }
}

//@ assignable p.text;
delegate void Formatter(Paragraph p);

class Formatters {
   //@ assignable p.text;
   public static void alignLeft(Paragraph p)
   { /* modify p.text */ }
   
   //@ assignable p.text;
   public static void alignRight(Paragraph p)
   { /* modify p.text */ }
}

An implementation of text paragraphs with two formatters. The formatter for a text paragraph is passed to the format method as a delegate. In this example, we have used Java and JML notation extended with C# delegates.

Example Code 2

class Paragraph {
   /*@ spec_public @*/ char[][] text;
   int width;

   //@ assignable text;
   public void format(Formatter f) {
      f.formatParagraph(this);
   }
}

interface Formatter {
   //@ assignable p.text;
   void formatParagraph(Paragraph p);
}

class AlignLeft implements Formatter {
   //@ also assignable p.text;
   public void formatParagraph(Paragraph p)
   { /* modify p.text */ }
}

class AlignRight implements Formatter {
   //@ also assignable p.text;
   public void formatParagraph(Paragraph p)
   { /* modify p.text */ }
}

An alternative implementation of the example using the Strategy pattern (in Java and JML).

Specification

Long Description

The example above shows a typical application of function objects. In this example, the format method of class Paragraph takes a delegate as an argument. This delegate represents a format algorithm that is applied to the text paragraph. Class Formatters provides two implementations of formatters that can be used to instantiate the delegate Formatter. The formatters format the text by directly modifying the text array of the Paragraph object. The second code example shows an alternative implementation using the Strategy pattern instead of a delegate.
Since different format algorithms can have very different behavior, we cannot completely specify their effect in an ensures clause of the Formatter delegate (or the formatParagraph method of the interface Formatter of example 2). This is typical for function objects. The various methods a function object can be instantiated with often have almost no common behavior that could be described in a specification of the function object. For instance, the update methods of different observers in the Observer pattern may react to an event completely differently. This distinguishes function objects from virtual methods with overriding implementations, where typically all implementations share some common behavior.
It is also not possible to give a direct and complete specification of the effect of format on a Paragraph object. Verifying such a specification would require knowledge about the effect of the invocation of the function object, but this knowledge is not available because the function object does not (and cannot) have a strong specification.
Since we cannot give a direct specification for format, we would like to specify its behavior relative to the behavior of the function object. In other words, we would like to specify that format applies the delegate instance f (or the method f.formatParagraph) to its receiver object. However, to use f in a mathematical description of the behavior of format one must summarize f’s behavior mathematically. This corelates with the problem of using method calls in specifications. In JML, using f directly in a specification would require that the delegate f be pure, and hence that all methods the delegate can be instantiated with also be pure. But this is not the case in our example since these methods modify the text array. Function objects that are non-pure methods are common and occur, for instance, in the cooperation between containers and layout managers in the Java Abstract Windowing Toolkit. Thus reasoning about function objects is an interesting research 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


Solution

Tool/Method

VeriFast

Code/Specification

/*@
predicate paragraph(Paragraph p, boolean isLeftFormatted) = p.text |-> ?text;
@*/

class Paragraph {
  String text;
  public void format(Formatter f) 
    //@ requires f!= null &*& formatter_run_pre(f.getClass())(f, this);
    //@ ensures formatter_run_post(f.getClass())(f, this);
  {
    f.run(this);
  }
}

/*@
predicate_family formatter_run_pre(Class c)(Formatter f, Paragraph p);
predicate_family formatter_run_post(Class c)(Formatter f, Paragraph p);
@*/

interface Formatter {
  void run(Paragraph p);
    //@ requires formatter_run_pre(this.getClass())(this, p);
    //@ ensures formatter_run_post(this.getClass())(this, p);
}

/*@
predicate_family_instance formatter_run_pre(AlignLeftFormatter.class)(AlignLeftFormatter f, Paragraph p) = 
  paragraph(p, false);

predicate_family_instance formatter_run_post(AlignLeftFormatter.class)(AlignLeftFormatter f, Paragraph p) = 
  paragraph(p, true);
@*/

class AlignLeftFormatter implements Formatter {

  AlignLeftFormatter() 
    //@ requires true;
    //@ ensures result != null;
  {
  }

  void run(Paragraph p) 
    //@ requires formatter_run_pre(AlignLeftFormatter.class)(this, p);
    //@ ensures formatter_run_post(AlignLeftFormatter.class)(this, p);
  {
    //@ open formatter_run_pre(AlignLeftFormatter.class)(this, p);
    Formatters.alignLeft(p);
    //@ close formatter_run_post(AlignLeftFormatter.class)(this, p);
  }
}

class Formatters {
  public static void alignLeft(Paragraph p) 
    //@ requires paragraph(p, false);
    //@ ensures paragraph(p, true);
  {
    //@ open paragraph(p, false);
    // do stuff
    //@ close paragraph(p, true);
  }
}

class Program {
  void apply_align_left(Paragraph p) 
    //@ requires p!= null &*& paragraph(p, false);
    //@ ensures paragraph(p, true);
  {
    AlignLeftFormatter alf = new AlignLeftFormatter();
    //@ close formatter_run_pre(AlignLeftFormatter.class)(alf, p);
    p.format(alf);
    //@ open formatter_run_post(AlignLeftFormatter.class)(alf, p);
  }
}

Solution-problem relationship

Interactivity, effort needed

How to reproduce

- run VeriFast on the corresponding .Java file

Published

Submitted by

jans