These notes will also address the early part of the program development cycle: the commissioning of a software system and the gradual, disciplined construction which takes place before the final realisation as a program.
The initial commissioning of a software system represents a contract between the software developer and the commissioner. Such a contract will ultimately give rise to a significant amount of taxing software development and the contract should describe with as much precision as possible the final behaviour of the desired software system. Even when a contract has been signed, how can the software developer ever show that the contracted software development was complete? This question is much more difficult than one might at first suspect. Even extremely short computer programs have so many possible input values that checking each of them would take an impossibly long time. How then is the correctness of a computer program ever to be established?
The Extended ML program development framework provides a specification language which is used to express the contract between the software developer and the client. A formal development method provides rules which allow the software developer to decide whether or not a proposed development step is correct.
The Extended ML language will be used here to specify problems whose solution is to be implemented in Standard ML. The Extended ML language can be used to express preliminary, non-executable descriptions of systems which are not yet built. Extended ML can also be used to describe the final, efficiently executable program using that part of the language which agrees precisely with Standard ML. The language can also be used to express all the intermediate designs and fabrications between the first specification and the final implementation. This wide range of uses for Extended ML leads it to be termed a wide spectrum language.
Most frequently, use of Extended ML is framed in relation to the module sublanguage of Standard ML and decomposition of large programs into units takes place along the module boundaries.