Modules are the computational counterpart of the abstract units, usually called tasks, in which a programmer decompose a complex problem solving task . This abstract units are characterised basically by the goal (query) they have to achieve. Hence, when designing a module the first decision is the goal, or the set of goals, that module will solve. In Milord II these goals are represented by the set of accessible facts of that module. Then, when designing a particularization of the module, that is, when filling it with more contents, we must keep the same set of goals, as far as the new module is still an implementation of the task that is being solved. The refinement operation guarantees that the new generated module fullfills this . Consider the following example that completes the example in the previous Section:
Module Sample = Begin Export DCGP, CGPC, CGPR, GNG, CBNG End Module Sputum_Gram : Sample = Begin Import Sputum_class, Sputum_Gram Export DCGP, CGPC, CGPR, GNG, CBNG Deductive knowledge Dictionary: ... Rules: R001 If Sputum_Gram = (DCGP_MC) then conclude DCGP is definite ... End deductive End
The module Sample only contains an export interface. The second expression declares that the module Sputum_Gram is a refinement of the module Sample.
This is the idea of incremental programming, all the modules that are refinements of the module Sample have the same export interface with, eventually, differences in other components that allows the module to obtain better, or different, results for the exported facts than the module Sample.
The refinement operation is specially useful when we declare generic modules. Remember that the instantiation of a generic module implies binding parameter names to submodules. The resultant module should use the exported facts of the submodules bound. It is obvious that not all the modules can be used to instantiate a generic module, because the code of the generic module will depend upon particular exported facts of those submodules. For instance, we could modify the previous declaration of the generic module Find_Germ as follows:
Module Find_Germ (X : Sample) = Begin ;;the same declarations that in the definition above End
This kind of declaration assure us that the modules used to instantiate the generic module Find_Germ are only those which are refinements of the module Sample, that is, that have exactly its same export interface (in particular, we can assure that any argument module will export the fact DCGP). So, usually, any generic module will have its parameters being a refinement of a very simple module containing just an interface. More complex requirements on the arguments can be imposed by filling with contents the module from which they have to be a refinement.
A refinement operation is the result of the composition of three
operations: enrichment verification, inheritance and information hiding.
We will explain these components keeping in mind the following equivalent
Module M = M_1 : M_2 Module M : M_2 = M_1
That means that the module M_1 can extend the export interface and the submodules of M_2. When a submodule is declared in both modules M_1 and M_2, they must preserve the enrichment relation.
When we define a refined version of a module, if we omit the body of a submodule, it will be inherited. Hence, the module M will inherit the bodies of the submodules of M_2 that not are present in the declaration of M_1. The inheritance operation makes a copy of the non redefined elements of the dictionaries. In the case of the local logic, the module inherits the logic of module M_2.
In a refinement operation, information hiding affects the export interface and the modular structure of the module created by the refinement. All the exported facts of M_1 not present in the export interface of M_2 are hidden in the resulting module M. Similarly all the submodules of M_1 not visible in the hierarchy of M_2 are hidden in the resulting module M.
Refinement is then defined as the combined action of these three operations. The other two relations between modules are slight variations of refinement.