By abstracting behavior and carefully engineering interfaces, software building blocks, also called generic components, can be produced that are more easily composable and widely usable than the specialized components usually constructed in current practice. Because of their potential uses, such components are subject to the most rigorous possible scrutiny, including applying formal methods of specification and proof of correctness. This project investigates two key issues involved in applying formal methods to construction and use of generic components: (1) the need for a formal specification language and related tools that fully support behavioral abstraction, and (2) the need to deal with practically useful components, in which efficiency as well as generality is a key concern. The language and tools issue is being addressed by development of the Tecton concept description language, its proof theory, and a Tecton parser, type-checker and semantic processor (for generating proof obligations); these tools are integrated into a previously developed interactive proof system. The usefulness issue is addressed by developing formal concepts and models in Tecton for highly optimized algorithms, such as generic sorting and searching algorithms taken from a C++ generic library.
