<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
             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.