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

Behavioral interface specification languages allow programmers to
express the intended behavior of programs such as functional behavior
and resource consumption. Formal specifications of program behavior is
useful for precise documentation, for the generation of test cases and
test oracles, for debugging, and for formal program verification. In
this paper, we survey behavioral interface specification languages
with a focus toward automatic program verification and, in particular,
the Verified Software Initiative.

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: Assertion, Bandera, Eiffel, interface specification
language, guarantee condition, invariant, JML, model checking,
postcondition, precondition, rely condition, separation logic, Spec#,
SPARK, temporal logic, VDM.

Submitted for publication.