Java Reference
In-Depth Information
The axiomatic approach is good for deriving proofs of programcorrectness
because it avoids implementation details and concentrates on how relations
among variables are changed by statement execution. Although axioms can
formalize important properties of the semantics of a programming language, it
is di
cult to use them to define most programming languages completely. For
example, they do not do a good job of modeling implementation considerations
such as running out of memory.
Denotational Semantics
Denotational models
[Sch86] aremore mathematical in form than operational
models, but they can accommodate memory stores and fetches that are central
to procedural languages. They rely on notation and terminology drawn from
mathematics, so they are often fairly compact, especially in comparison with
operational definitions.
A denotational definition may be viewed as a syntax-directed definition
that specifies the meaning of a construct in terms of the meaning of its immedi-
ate constituents. For example, to define addition, we might use the following
rule:
E
[
T
1
+
T
2]
m
=
E
[
T
1]
m
+
E
[
T
2]
m
This definition says that the value obtained by adding two subexpressions,
T
1and
T
2, in the context of a memory state
m
is defined to be the sum of
the arithmetic values obtained by evaluating
T
1 in the context of
m
(denoted
E
[
T
1]
m
)and
T
2 in the context of
m
(denoted
E
[
T
2]
m
).
Denotational techniques are quite popular and form the basis for rigorous
definitions of programming languages. Research has shown that it is possible
to convert denotational representations
automatically
to equivalent representa-
tions that are directly executable [Set83, Wan82, App85].
Summary
Regardless of how semantics are specified, our concern for pre-
cise semantics is motivated by the fact that writing a complete and accurate
compiler for a programming language requires that the language itself be well
defined. While this assertion may seem self-evident, many languages are
defined by imprecise or informal language specifications. Attention is often
given to formal specification of
syntax
, but the
semantics
of the languagemay be
defined via informal prose. The resulting definition inevitably is ambiguous
or incomplete on certain points.
For example, in Java all functions must return via a return
expr
state-
ment, where expr is assignable to the function's return type. The following is
therefore illegal:
