Refinement

The most striking construct of Elan is the <#1531#>refinement<#1531#>, a simple mechanism for defining abstract algorithms which forms the basis for the <#1532#>Top-Down<#1532#> programming style, which can be summarized:

``A program is developed by first giving a rough but potentially correct formulation composed of abstract entities. Thereupon each of these abstract entities is similarly defined, in terms of other abstract and concrete entities, until at last all necessary abstract entities have a suitable definition.''

A refinement gives a name to a paragraph, and looks like


#litout1708#

Executing the name of a refinement means executing its constituent paragraph (its <#1537#>body<#1537#>). The value of the refinement is the value of its body.

In distinction to procedures (which could also in principle be used as refinements) refinements may appear in any order, and may in particular appear after any invocation of the refinement. Refinements can not have parameters, in order to keep the ``visual overhead'' in their definition and application to a minimum. A refinement does not form a separate scope of naming. Therefore it is possible to put a declaration in one refinement and use it in another. For these reasons, refinements are better suited than procedures for capturing the ``fleeting abstractions'' in programming.

In Elan-0, a program consists of one or more refinements, where the first refinement is the <#1538#>root<#1538#> of the program. Such programs correspond to procedure-bodies in full Elan.