Expansion allows to build modules as an extension of a previous version. We can extend the set of accessible facts or add submodules to the previous version. As in the refinement case to expand modules we test that the new module is an enrichment of the previous one. Inheritance of components is performed as in the refinement operation, but information hiding is not applied.
In the next example, we are forcing the argument of a generic module Generic to have at least the export predicates of Type in their export interface.
Module Generic (X > Type) = Begin ... End
So, the generic module will be applicable over a wider range of modules than if its argument was defined as a refinement of Type.
Contraction only test an inverse enrichment verification. Given the declaration Module M = M_1 < M_2 we only test that M_2:M_1 holds. It is not necessary to apply information hiding because the module M_1 exports less facts than M_2. Inheritance of components is performed as in the refinement operation.