Date Added: Jul 2011
Delegation is a very common programming idiom, whereby a task is carried out by a statically unknown part of the program. Delegation enhances the modularity and the extensibility of a program, and, for that reason, is the main ingredient of many important design patterns. Unfortunately, delegation complicates specification and verification: the programmer must either rely on unsuitably weak specifications imposed by behavioral sub-typing, or compromise automation by resorting to higher-order logic. In this paper, the authors present an expressive specification and verification methodology, in which partial correctness reasoning about delegation can be carried out in first order logic, using automated SMT solvers.