Overview of Programming Language Semantics

Semantics refers to the meaning we associate with programming language constructs.

Most often, programming language semantics is described informally, in terms of the operations necessary to execute language constructs in terms of basic computer actions (using a simplified or abstract computer model).

Formal approaches use mathematical and logical techniques to more precisely define language semantics. There are two basic approaches:

1. Property based.
   Here, the aim of a formal method is to tell us how we can reason about the properties of programs written in the language. In particular, axiomatic semantics refers to the use of axioms and rules of inference to derive true statements about the properties of programs.
2. Model based.
   Here the formal method describes the semantics of a language in terms of a model.
   1. Formal operational semantics.
      The execution of language constructs is mathematically described in terms of the formalized operations of an abstract machine.
   2. Denotational semantics.
      The meaning of language constructs is defined by modelling them as mathematical objects, usually functions. For example, statements are modelled as functions which transforms mathematical "computer states" into new computer states, and an assignment statement is modelled by a function in which the output computer state is similar to the input computer state except for the contents of one location in the state.
   3. Translational semantics: the semantics of a language is described by showing how it translates to another, presumably well understood, language. Sometimes a translational approach is used to define a full language in terms of a core subset of the language. A denotational or operational definition is then only required for the core language, potentially a much smaller task.

Why Formal Semantics?

1. For precise language description.
   English descriptions almost always have ambiguities and omit various details. This can make it hard for programmers to determine what the meaning of a particular construct is.
2. For language standardization.
   Imprecise descriptions allow language implementors to interpret the language differently and hence come up with incompatible implementations. A program that is correct in one environment does not behave as expected elsewhere. People who learn a language in one environment may not use the language correctly in a different one. Standardization promotes the portability of programs and people.
3. For language designers.
   Mathematically modelling a proposed language design often allows flaws to be exposed. Complete mathematical models help ensure that all aspects of language design are taken care of.
4. To support formal reasoning about programs.
   Formal semantic descriptions allow properties of programs to be analyzed. In particular, it may be possible to formally verify that a program meets its input-output specifications