Refinement

Modules are the computational counterpart of the abstract units, usually called tasks, in which a programmer decompose a complex problem solving task [9]. 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 [15]. 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 syntactic declarations:
Module M = M_1 : M_2 Module M : M_2 = M_1

Enrichment Verification

We say that the module M_1 is an enrichment of the module M_2, if and only if:

1. The export interface of M_2 is a subset of the export interface of M_1.
2. The submodule names of M_2 are a subset of the submodule names in M_1. If a submodule name is bound both in M_2 and M_1, the modules to which it is bound, let's say M_21 M_11, must satisfy that either M_11 is an empty body, or otherwise M_11 must be an enrichment of M_21.
3. The local logic declaration must be the same; or empty in M_2.

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.

Inheritance

When we declare a module as a refinement of another we usually want to maintain several components of the module being refined. To avoid the programmer to write the components to be preserved twice, an inheritance mechanism is provided in Milord II. The components of a module that can be inherited are: submodules, fact definitions and local logics.

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.

Information Hiding

One of the conditions that the modules have to fulfill to satisfy a refinement relation is that the accessible facts of both modules must be the same. So, after checking the enrichment of information, Milord II hides all new accessible facts and new submodules of the refined module (if any).

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.