Functional Containers for Specification in SPARK

This technical paper discusses the implementation of functional containers for specification in the SPARK tool, which is designed for static analysis of Ada programs. The SPARK tool verifies that programs are free from runtime exceptions and conform to specified contracts. The paper outlines the limitations of the existing Ada contract annotation language and introduces the functional containers library, which provides collections suitable for use in specifications. It details how these containers can enhance the specification and verification of complex programs through concrete examples. The paper also describes the compatibility of these libraries with the SPARK tool, emphasizing the use of reusable specification features rather than hard-coded mappings. Additionally, it explains the differences between standard Ada containers and SPARK-compatible formal containers, highlighting the importance of contracts in deductive verification. The functional containers are designed to be lightweight and efficient for specification purposes, allowing for easier program verification.