Modular verification of higher-order methods with mandatory calls specified by model programs







Deposit Papers 


Shaner, Steve (2009) Modular verification of higher-order methods with mandatory calls specified by model programs. Technical Report 09-16, Computer Science, Iowa State University.

Full text available as:Adobe PDF

This is the latest version of this eprint.


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.

Subjects:Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
ID code:00000593
Deposited by:Steve Shaner on 05 March 2009

Available Versions of This Paper

Contact site administrator at: