Modular Verification of Higher-Order Methods
	   with Mandatory Calls Specified by Model Programs
				  by
	Steve M. Shaner, Gary T. Leavens, and David A. Naumann

			       Abstract

What we call a ``higher-order method'' (HOM) is a method that makes
mandatory calls to other dynamically-dispatched methods.  Examples
include template methods as in the Template method design pattern and
notify methods in the Observer pattern.  HOMs are particularly
difficult to reason about, because standard pre- and postcondition
specifications cannot describe the mandatory calls.  For reasoning
about such methods, existing approaches use either higher-order logic
or traces, but both are complex and verbose.

We describe a simple, concise, and modular approach to specifying HOMs
We show how to verify calls to HOMs and their code using first-order
verification conditions, in a sound and modular way.

Verification of client code that calls HOMs can take
advantage of the client's knowledge about the mandatory calls to make
strong conclusions.  Our verification technique validates and explains
traditional documentation practice for HOMs, which typically shows
their code.  However, specifications do not have to expose all of the
code to clients, but only enough to determine how the HOM makes its
mandatory calls.

Keywords: Model program, verification,
specification languages, grey-box approach, higher order method, 
mandatory call, Hoare logic, refinement calculus.

2006 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, methodologies;
D.2.4 [Software Engineering]
        Software/Program Verification --- correctness proofs, formal methods, 
        programming by contract;
D.3.3 [Programming Languages]
	Language Constructs and Features --- abstract data types, 
        classes and objects, control structures, frameworks, 
        procedures, functions, and subroutines;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
        assertions, logics of programs, pre- and post-conditions, 
        specification techniques.