Generic programming in the mCRL2 toolset

The mCRL2 tool set [GKM+08] is a tool set for verification and validation of concurrent processes, based on process algebra speci??cations. The mCRL2 language is based on the Algebra of Communicating Processes (ACP), which is extended to include data and time. This paper reports on experiences with generic programming in C++ as applied in the implementation of the tool set. C++ concepts, a type system for templates [RS06], form a key ingredient of this style of programming. Using concept definitions, requirements on template types can be defined that are type checked during compile time. The main benefits for the mCRL2 tool set are uniform and exible interfaces that operate on well-defined types, and a signi??cant increase in code reuse. The use of concepts also promotes the writing of code that corresponds closely to pseudo code, since the chosen concepts correspond naturally with domain specific concepts. This will be illustrated by a simple use case, namely substitution functions. Generic programming is about generalizing software components, to enable reuse in a wide variety of situations. In C++, generic programming is enabled using templates. C++ concepts are proposed as a means to type check template types. A concept is a set of requirements (valid expressions, associated types, semantic invariants, complexity guarantees, and so on) that a type must fulfill to be correctly used as an argument in a call to a generic algorithm, see [RS06]. Language support for concepts has been proposed [GJS+06] for the next version of the C++ standard, C++0x. Concepts will be used to make the specification of the C++ standard library more complete and precise. A derivative of the GNU C++ compiler [Gre08] already implements language support for concepts. In the mCRL2 tool set we have used a portable library for concept checking. Most uses of generic programming in general, and more specifically the use of concepts, that are described in the literature treat the construction of data structures and algorithms that operate on these, see e.g. [GL05]