Behavioral Interface Specification Languages
Abbreviated Journal Title
ACM Comput. Surv.
Keywords
Design; Documentation; Reliability; Verification; Abstraction; assertion; behavioral subtyping; frame conditions; interface; specification language; invariant; JML; postcondition; precondition; separation logic; Spec#; SPARK; OBJECT-ORIENTED PROGRAMS; TEMPORAL LOGIC; VERIFYING COMPILER; SEPARATION; LOGIC; DYNAMIC FRAMES; MODULAR SPECIFICATION; CONCURRENT PROGRAMS; ASSERTION CHECKING; SYMBOLIC EXECUTION; AUTOMATIC VERIFIER; Computer Science, Theory & Methods
Abstract
Behavioral interface specification languages provide formal code-level annotations, such as preconditions, 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 article 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.
Journal Title
Acm Computing Surveys
Volume
44
Issue/Number
3
Publication Date
1-1-2012
Document Type
Article
Language
English
First Page
58
WOS Identifier
ISSN
0360-0300
Recommended Citation
"Behavioral Interface Specification Languages" (2012). Faculty Bibliography 2010s. 2725.
https://stars.library.ucf.edu/facultybib2010/2725
Comments
Authors: contact us about adding a copy of your work at STARS@ucf.edu