Modular Verification Scopes via Export Sets and Translucent Exports

Abstract

Following software engineering best practices, programs are divided into modules to facilitate information hiding. A variety of programming-language constructs provide ways to define a module and to classify which of its declarations are private to the module and which are available to public clients of the module. Many declarations can be viewed as consisting of a signature and a body. For such a declaration, a module may want to export just the signature or both the signature and body. This translucency is particularly useful when formally verifying a program, because it lets a module decide how much of a declaration clients are allowed to depend on. This article describes a module system that supports multiple export sets per module. Each export set indicates the translucency of its exported declarations. The module system is implemented as part of the verification-aware programming language Dafny. Experience with the module system suggests that translucency is useful.