4. Semantics

Semantics

The semantics of a language defines the meaning of programs, how they behave when they are executed on a computer.

Link to original

There are two kinds of semantics:

• Static Semantics

  Static Semantics (typing): detect (before execution) that programs that are syntactically correct but will give errors during execution

  Link to original

• Dynamic Semantics

  Dynamic Semantics (or just Semantics): specifies meaning of programs

  Link to original

Informal Semantics

Informal semantics are descriptions in natural language.

Link to original

Formal Semantics

Formal semantics are precise and important for:

• implementation of the language; behaviour of each construct is specified providing an abstraction of the execution process which is independent of the machine
• programmers: formal semantics provides tools / techniques to reason about programs
• language designers: allows to detect ambiguities in the constructs and suggest improvements and new constructs

Link to original

Formal semantics can be quite complex so usually only a part of the language is formally defined.

There are different styles of semantics:

• Denotational Semantics: meaning of expressions (and in general, constructs) is given in an abstract, mathematical way.
• Axiomatic Semantics: uses axioms and deduction rules in a specific logic. Predicates or assertions are given before and after each construct, describing the constraints on program variables before and after execution of a statement.
• Operational Semantics: the meaning of each construct is given in terms of computation steps; the behaviour of the program during execution can be described using a transition system.

We study operational semantics in this course. Operational is useful for implementation and proving correctness of compiler optimisation. Denotational / axiomatic are useful to reason and prove properties of programs.

Transition Systems

Transition System

A transition system is specified by:

• a set $\text{Config}$ of configurations or states
• a binary relation $\to \subseteq \text{Config}\times \text{Config}$ called a transition relation we use the notation $c\to c^{\prime }$ (infix) to indicate that $c$, $c^{\prime }$ are related by $\to$

Link to original

Deterministic Transition System

A transition system is deterministic if for all $c,c_1,c_2$: $c\to c_1\text{ and }c\to c_2\text{ implies }{c}_1=c_2$

Link to original

Notation

Additional notes on notation:

• $c\to c^{\prime }$ denotes a transition / change of state from $c$ to $c^{\prime }$
• $c{\to }^{\ast }{c}^{\prime }$ is the reflexive transitive closure of $\to$ it holds iff there is a sequence of transitions: $c\to c_1\to \dots \to c_n=c^{\prime }$ where $n\ge 0$

We distinguish an initial and final (terminal) subset of configurations, written $I$ and $T$. For all $c\in T$, there is no $c^{\prime }$ such that $c\to c^{\prime }$. The idea is that a sequence of transitions from $i\in I$ to $t\in T$ represents a run of the program.

Abstract Machines

An abstract machine is a transition system that specifies an interpreter for a programming language.

It is an abstraction of a computer, describing how the program will execute. For a real programming language, these descriptions can be large and complicated.