Specifying And Verifying Advanced Control Features

Keywords

Greybox specification; JML language; Modular verification

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.

Publication Date

1-1-2016

Publication Title

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Volume

9953 LNCS

Number of Pages

80-96

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1007/978-3-319-47169-3_7

Socpus ID

84994048432 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/84994048432

This document is currently not available here.

Share

COinS