Behavioral Interface Specification Languages 
                                  by
          John Hatcliff, Gary T. Leavens, K. Rustan M. Leino,
                 Peter Mueller, and Matthew Parkinson
                                   
                               Abstract

Behavioral interface specification languages provide formal code-level
annotations such as pre-/postconditions, invariants, and assertions
that allow programmers to express the intended behavior of program
modules.  Such specifications are useful for precisely documenting
program behavior, for guiding implementation, and for facilitating
agreement between teams of programmers in modular development of
software.  When used in conjunction with automated analysis and
program verification tools, such specifications can support detection
of common code vulnerabilities, capture of light-weight
application-specific semantic properties, generation of test cases and
test oracles, and full formal program verification.  This paper
surveys behavioral interface specification languages with a focus
toward automatic program verification, and with a view towards aiding
the Verified Software Initiative---a fifteen-year, cooperative,
international project directed at the scientific challenges of
large-scale software verification.

2008 CR Categories:

D.2.1 [Software Engineering]
    Requirements/Specifications --- Languages;
D.2.4 [Software Engineering]
    Software/Program Verification --- Assertion checkers, 
      class invariants, formal methods, 
      model checking, programming by contract, reliability, validation;
F.3.1 [Logics and Meanings of Programs]
    Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, pre- and post-conditions,
                specification techniques.

Keywords: Abstraction, assertion, behavioral subtyping, frame conditions,
 interface specification language, invariant, JML, 
postcondition, precondition, separation logic, Spec#,
SPARK.

Submitted for publication.