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