We discuss formal specification and verification in a generic context. Our view is that generic entities, such as templates or generic program components, may benefit from applications of formal methods even more than non-generic ones since often their correctness crucially depends on parameters being properly instantiated; thus the formal specification of semantic requirements on parameters and the verification that instantiations satisfy those constraining requirements is essential.
The talk builds on the experience gained in building up a collection of generic theories for programming language semantics and compilation of simple Pascal-like languages, in the context of project Verifix. The basic theories include a development of the required mathematics, including domain theory, fixed-point theory and fixed-point induction; denotational semantics for elementary programming constructs and, derived from this, other forms of semantics. The compilation theories are structured into several conceptually different levels (identifiers and variables, expressions, control structures) in such a manner that each level abstracts as much as possible from details of the lower ones. In all theories, special emphasis is given to modularity and genericity to maximize the degree of reusability. The vehicle for the formal development is the PVS system; we discuss to what extent PVS provides appropriate mechanisms for achieving the desired level of genericity.
Although this work addresses issues of generic programming only in a rather restricted domain (compilation), we believe that both the approach to generic specification and verification and the mathematical theories developed so far provide us with a model that will be applicable to the formal treatment of a much wider variety of generic programming problems.