.png){kind=icon}
.png){kind=icon}
Return
Behavioral Interface Specification Languages
.png){kind=icon}
PRE
AI
DOI：10.1145/2187671.2187678.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
Design
Documentation
Reliability
Verification
Abstraction
assertion
behavioral subtyping
frame conditions
interface specification language
invariant
JML
postcondition
precondition
separation logic
Spec#
SPARK
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
28
Papers:
2.4K
Citations:
3.5W
View more organizations