Information Technology Reference
In-Depth Information
the same programming language should be a rigorous scientic criterion of the
maturity of a theory and of a language, when deciding whether it is ready for
practical implementation and widespread use.
2 Top-Down
A top-down presentation of a theory of programming starts with an account
of a conceptual framework appropriate for the description of the behaviour of a
running program as it may be observed by its users. For each kind of observation,
an identier is chosen serve as a variable whose exact value will be determined
on each particular run of the program. Variables whose values are measured
as a result of experiment are very familiar in all branches of natural science;
for example in mechanics,
is often declared to denote the displacement of a
particular object from the origin along a particular axis, and _
x
x
denotes the rate
x
of change of
. We will nd that such analogies with the normal practice of
scientists and engineers provide illumination and encouragement at the start as
well as later in the development of theories of programming.
There are two special times at which observation of an experiment or the run
of a program are especially interesting, at the very beginning and at the very
end. That is why the specication language VDM introduces special superscript
arrow notations:
x to denote the initial value of the global program variable
,and !
x
to denote its nal value on successful termination of the program.
(The Z notation uses
x
x 0 for these purposes). Fragments of program in
dierent contexts will update dierent sets of global variables. The set of typed
variables relevant to a particular program fragment is known as its alphabet .In
the conventional sequential programming paradigm, the beginning and the end
of the run of a program are the only times when it is necessary or desirable
to consider the values of the global variables accessed and updated by it. We
certainly want to ignore the millions of possible intermediate values calculated
during its execution, and it is a goal of the theory to validate this simplication.
A full understanding of a description of program behaviour requires prior
specication of its alphabet, and agreement on the way in which the value of
each variable in it can be determined by experiment. To interpret the meaning
of a program without knowing its alphabet is as impossible as the interpretation
of a message in information theory without knowing the range of message values
that might have been sent instead. Not all the relevant parameters of program
behaviour have to be directly observable from outside the computer; some may
be observable only indirectly, by their eect on other programs. Actually, even
the values of the program variables inside the computer are inaccessible to a
user; they can be controlled or observed only with the aid of an input-output
package, which is written in the same language as the program under analysis.
The indirect observations are needed to make successful predictions about the
behaviour of larger programs, based on knowledge of the behaviour of their
components parts.
x
and
Search WWH ::




Custom Search