Specifying and Verifying Advanced Control Features
Date
2016-10-05
Authors
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Springer, Cham
Abstract
Advances in programming often revolve around key design patterns, which programming languages embody as new control features. These control features, such as higher-order functions, advice, and context dependence, use indirection to decrease coupling and enhance modularity. However, this indirection makes them difficult to verify, because it hides actions (and their effects) behind an abstraction barrier. Such abstraction barriers can be overcome in a modular way using greybox specification techniques, provided the programming language supports interfaces as a place to record specifications. These techniques have previously allowed specification and modular verification of higher-order functional and object-oriented programs, as well as aspect-oriented and context-oriented programs.
Series Number
Journal Issue
Is Version Of
Versions
Series
Academic or Administrative Unit
Type
Presentation
Comments
This is a post-peer-review, pre-copyedit version of a proceeding published as Leavens, Gary T., David Naumann, Hridesh Rajan, and Tomoyuki Aotani. "Specifying and verifying advanced control features." In International Symposium on Leveraging Applications of Formal Methods, pp. 80-96. Springer, Cham, 2016. The final authenticated version is available online at DOI: 10.1007/978-3-319-47169-3_7. Copyright 2016 Springer International Publishing AG. Posted with permission.