A Basis for Formal Specification and Verification of Generic Algorithms in the C++ Standard Template Library

Generic algorithms are algorithms designed to work with a variety of data structures. A software library in which most algorithms are generic can thus provide very extensive capabilities with a relatively small amount of source code. The high initial cost of applying formal methods to generic components becomes reasonable when amortized over the many different uses that can later be made. This paper is an attempt to provide a foundation for formal specification and verification of generic algorithms, paying particular attention to supporting the techniques by which generality is achieved in the C++ Standard Template Library. Axioms and inference rules are presented that support reasoning about essentially all the C++ language features and STL programming techniques used in the library's generic algorithms. Examples of applications to several simple STL generic algorithms are given. Categories and Subject Descriptors: D.2.2. [Software Engineering]: Tools and Techniques---software librar..