Theories, parameterized modules, and views are the basic building blocks of parameterized programming [9,44]. As in OBJ, a theory defines the interface of a parameterized module, that is, the structure and properties required of an actual parameter.
A parameterized module is a module with one or more parameters, each of which is expressed by means of one theory, that is, modules can be parameterized by one or more theories. If we want, e.g., to define a list or a set of elements, we may define a module LIST or SET parameterized by a theory expressing the requirements on the type of the elements to store in such data structures. Thus, theories are used to declare the interface requirements for parameterized modules. In the case of lists and sets we do not need any requirement on the data elements, and therefore we may use the trivial theory TRIV, with just a sort Elt, as parameter of such modules; but in other cases, say search trees or sorted lists, we may require, e.g., a particular operator, an order relation, or an equivalence relation, in which cases we shall need to use the appropriate theories describing the specific requirements.
The instantiation of the formal parameters of a parameterized module with actual parameter modules or theories requires a view mapping entities from the formal interface theory to the corresponding entities in the actual parameter module.