Title
Specifying and Verifying Advanced Control Features.
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.
Year
DOI
Venue
2016
10.1007/978-3-319-47169-3_7
Lecture Notes in Computer Science
Keywords
Field
DocType
Greybox specification,Modular verification,JML language
Indirection,Abstraction,Programming language,Computer science,Software design pattern,Modular design,Modularity
Conference
Volume
ISSN
Citations 
9953
0302-9743
2
PageRank 
References 
Authors
0.37
15
4
Name
Order
Citations
PageRank
Gary T. Leavens12593211.29
David Naumann2110184.12
Hridesh Rajan382059.44
Tomoyuki Aotani416718.97