Information Technology Reference
In-Depth Information
{
A bottom-up presentation of a theory of programming gives excellent sup-
port for reasoning about the execution of programs that have already been
written. By starting with a denition of the individual steps of execution, it
models directly the run-time eciency of programs. Execution traces provide
the primary diagnostic information on debugging runs of incorrect programs.
On the other hand, an operational semantics gives no help at all in relating
a program to its intended purpose. It is therefore useless in reasoning about
programs before they have been written in the notations of a particular
programming language.
If programming theory is ever to make its full contribution to the practice
of programming, we must oer all the benets of both styles, and none of the
deciencies. Neither approach could be recommended by itself. It is clearly foolish
to provide a conceptual framework for program design if there is no way of
executing the resulting program step by step on a computer. It would be equally
unsatisfactory to present an operationally dened theory if there is no way of
describing what a program is intended to do.
In the natural sciences, it is a necessary condition of acceptability of a the-
ory that it should agree with experiment. Experiments are equally important in
validation of theories of programming. They test the eciency with which a new
programming concept can be implemented and the convenience with which it
can be used. An experiment which requires the design, implementation and use
of a completely new programming language is prohibitively time-consuming. For
rapid scientic progress, it is preferable just to add a single new feature to an
existing programming language, its compiler and its run time system. The rst
trial applications may be conducted by a group of experimental programmers,
who have accepted the risk that the new feature may soon be changed or with-
drawn. Even such a limited experiment is expensive; and worse, it is dicult to
interpret the results, because of uncontrollable factors such as the skill and the
experience of the people involved.
That is why it is advisable to restrict experimentation to test only theories
that have shown the highest initial promise. The promise of a theory is not judged
by its popularity or by its novelty or by its protability in competition with rival
theories. Quite the reverse: it is by its coherence and close agreement with other
theories that a new theory can be most strongly recommended for test. Such
agreement is much more impressive if the theories are presented in radically
diering styles. From the practical point of view, it is the stylistic dierences
that ensure complementarity of the benets to the user of the programming
language. And the results of the experiment are much more convincing if the
implementors and trial users are completely independent of the original theorists,
as they usually are in more mature branches of Science.
The unication of theories is not a goal that is easy to achieve, and it often
requires a succession of adjustments to the details of the theories, and in the way
they are tested. The development of an abstract denotational model to match a
given operational semantics is known as the problem of full abstraction. It took
many years to discover fully abstract models for PCF, a simple typed functional
Search WWH ::
Custom Search