Modular verification of higher-order methods with mandatory calls specified by model programs by Steve M. Shaner Abstract Formal specification languages improve the flexibility and reliability of software. They capture program properties that can be verified against implementations of the specified program. By increasing the expressiveness of specification languages, we can strengthen the argument for adopting formal specification into standard programming practice. The higher-order method (HOM) is a kind of method whose behavior critically depends on one or more mandatory calls in its body. Programmers using HOMs would like to reason about the HOM's behavior, but revealing the entire code for such methods restricts writers of HOMs to a specific implementation. This thesis presents a simple, intuitive extension of JML, a formal specification language for Java, that enables client reasoning about the behavior of HOMs in a sound and modular way. Furthermore, our particular technique is capable of fully automatic checking with lower specification overhead than previous solutions. Supporting client reasoning about HOMs enables formal verification of some of the behavioral properties of HOM-using object-oriented design patterns, like Observer and Template Method. The technique also applies to specifying HOM behavior in any procedural language. 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. Copyright (c) 2008 by Steve M. Shaner All rights reserved.