archives

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


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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

There is a later version of this eprint available: Click here to view it.

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.
Subjects:Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
ID code:00000590
Deposited by:Steve Shaner on 26 January 2009

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu