Behavioral Interface Specification Languages

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,...

Full description

Saved in:
Bibliographic Details
Published in:ACM computing surveys 2012-06, Vol.44 (3), p.1-58
Main Authors: HATCLIFF, John, LEAVENS, Gary T, LEINO, K. Rustan M, MULLER, Peter, PARKINSON, Matthew
Format: Article
Language:English
Subjects:
Applied sciences
Behavior
Codes
Computer science
control theory
systems
Computer systems performance. Reliability
Exact sciences and technology
Interfaces
Programming languages
Software
Software engineering
Studies
Systems development
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0360-0300
1557-7341
DOI:10.1145/2187671.2187678