In
theoretical computer science, formal semantics is the field concerned with the rigorous mathematical study of the meaning of
programming languages and models of
computation. The formal semantics of a language is given by a
mathematical model that describes the possible computations described by the language. There are many approaches to formal semantics; these approaches belong to three major classes:
Denotational semantics, whereby each phrase in the language is translated into a denotation, i.e. a phrase in some other language. Denotational semantics loosely corresponds to
compilation, although the "target language" is usually a mathematical formalism rather than another computer language. For example, denotational semantics of
functional languages often translates the language into
domain theory;
Operational semantics, whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds to
interpretation, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define an
abstract machine (such as the
SECD machine), and give meaning to phrases by describing the transitions they induce on states of the machine. Alternatively, as with the pure
lambda calculus, operational semantics can be defined via syntactic transformations on phrases of the language itself;
Axiomatic semantics, whereby one gives meaning to phrases by describing the
logical axioms that apply to them. Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaning is exactly what can be proven about it in some logic. The canonical example of axiomatic semantics is
Hoare logic.
See more at Wikipedia.org...
Free Download Now!
