Open access
Date
2010Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
Closures, first-class citizen procedures that are able to capture their lexical environment, increase the expressiveness of objectoriented languages such as C#, Scala, and various dynamic languages. However, closures make program specification and verification more difficult. For instance, a verification methodology must allow specifications to describe the behavior of one method relatively to the specification of another method passed as argument, and it must allow specifications to describe the behavior of a closure without exposing its captured state. This paper presents a modular specification and partial correctness verification methodology for closures. Our solution is based on first-order logic and, thus, well suited for automatic verification with SMT solvers. We present an encoding of our methodology in the Boogie program verifier. Using this encoding, we have verified a series of interesting examples that cover the main applications of closures such as delegation patterns and even the creation of custom control flow. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006843251Publication status
unpublishedJournal / series
Technical Report / ETH Zurich, Department of Computer ScienceVolume
Publisher
ETH, Department of Computer ScienceSubject
SPEZIFIKATIONEN (SOFTWARE ENGINEERING); VERIFICATION (SOFTWARE ENGINEERING); OBJECT-ORIENTED PROGRAMMING (PROGRAMMING METHODS); SPECIFICATIONS (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING); OBJEKTORIENTIERTE PROGRAMMIERUNG (PROGRAMMIERMETHODEN)Organisational unit
03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science
Notes
Technical Reports D-INFK.More
Show all metadata
ETH Bibliography
yes
Altmetrics