Date Added: Dec 2009
Closures, first-class citizen procedures that are able to capture their lexical environment, increase the expressiveness of object-oriented 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.