Containers for specification in SPARK

Abstract The SPARK tool analyzes Ada programs statically. It can be used to verify both that a program is free from runtime exceptions and that it conforms to a specification expressed through contracts. To facilitate dynamic analysis, Ada contracts are regular Ada expressions which can be evaluated at execution. As a result, the annotation language of the SPARK tool is restricted to executable constructs. In this context, high-level concepts necessary for specification by contracts need to be supplied as libraries. For example, the latest version of the Ada language introduces unbounded integers and rational numbers to the standard library. In this article, we present the functional containers library, which provides collections suitable for use in specification. We then explain how they can be used to specify and verify complex programs through concrete examples that have been developed over many years. Finally, we describe how these libraries are supported in the SPARK tool using reusable specification features instead of built-in support, i.e., a hard-coded mapping of library functionalities to axiomatized theories for the underlying provers.