VDM Semantics of Programming Languages: Combinators and Monads - Formal Methods and Hybrid Real-Time Systems - page 485

(since the value of a compound numeral such as 100 can then be computed by
doubling the value of 10 , whereas with grouping to the right the value of 100
depends on the length of 00 as well as on its value, so denotations would then
be pairs of numbers).
Phrase structure for use in denotational semantics is specified by some form
of context-free grammar, together with a correspondence relating program texts
uniquely to derivation trees according to the grammar. The grammar could
be an unambiguous concrete grammar, involving the symbols used in program
texts; but usually it is an abstract grammar , defining a set of abstract syntax
trees whose structure is significantly simpler than that of derivation trees for a
concrete grammar. The relationship between program texts and abstract syntax
trees is generally left to be inferred from the use of suggestive symbols in the
abstract grammar, augmented by some informal explanations.
Semantic functions, mapping phrases to their denotations, are defined on ab-
stract syntax trees. The semantic function for a particular language is specified
inductively, by giving for each production of the abstract grammar a semantic
equation of the form:

M [[ ··· V 1 ··· V n ··· ]] = f ( M [[ V 1 ]] ,..., M [[ V n ]] ) ( 1 )

where V 1 ,...,V n are metavariables ranging over sets of abstract syntax trees,
and f expresses how the denotations

M

[[ V 1 ]] ,...,

M

[[ V n ]] of the subphrases are

composed to give the denotation of the phrase ' '. The double

brackets '[[ ... ]]' enclose the notation expressing syntactic phrases of the described
programming language, separating it from the notation used for expressing the
mathematical entities used as denotations.

··· V 1 ··· V n ···

Program behaviour: Program behaviour is an abstract representation of what is
supposed to be observable when programs are compiled and run. It corresponds
to the behaviour exhibited by conforming implementations of the programming
language.
Compilation usually involves checking for consistency between declaration
and use of identifiers throughout the program; the abstract behaviour might
then include a list of error messages, or merely a boolean value.
When running the program, its input and output are regarded as observable,
so its abstract behaviour always has to represent the input-output relationship.
In contrast, potentially observable properties such as how long it takes to run the
program (when it terminates), how much memory is required, which machine is
used, etc., are generally regarded as irrelevant to the conformance of implemen-
tations, and therefore not included in the abstract behaviour of programs.

Denotations: After a phrase structure has been chosen, the denotations of phrases
can be specified, subject only to the following constraints:

- the denotation of each phrase is composed from the denotations of its sub-
phrases, and
- the abstract behaviour of each program is determined by its denotation.