Explicit summary of the mapping between module types and our specification rules
At the end of the lectures on generic modules, circle back to the different types of modules and how the different types are implemented in our specification language. Use the following idea:
If the module has state variables and is defined with just the word module, you implement it as an abstract object. This means using the @staticmethod.
If the module has state variables and is defined with the words template module, you implement it as an ADT. The implementation will be a typical class in an OO language.
If the module does not have state variables, then it is a library. A library might export functions, types, constants etc. The types defined in this context will not be ADTs, but they could be record types, or enumerated types.
A generic module will be parameterized on the types. Although I suppose a library could be parameterized, we've only used examples of generic abstract objects and generic abstract data types.
The above description should make explicit the mapping between the types of modules given in Ghezzi et al, Chapter 4 (records, libraries, abstract objects, abstract data types and generic modules).