Thumbnail
Access Restriction
Subscribed

Author Hatcliff, John ♦ Leavens, Gary T. ♦ Leino, K Rustan M. ♦ Mller, Peter ♦ Parkinson, Matthew
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2012
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Abstraction ♦ JML ♦ SPARK ♦ Spec# ♦ Assertion ♦ Behavioral subtyping ♦ Frame conditions ♦ Interface specification language ♦ Invariant ♦ Postcondition ♦ Precondition ♦ Separation logic
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.
ISSN 03600300
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2012-06-01
Publisher Place New York
e-ISSN 15577341
Journal ACM Computing Surveys (CSUR)
Volume Number 44
Issue Number 3
Page Count 58
Starting Page 1
Ending Page 58


Open content in new tab

   Open content in new tab
Source: ACM Digital Library