Semantics: operational and denotational

Lesson 2 settled which strings are programs. This lesson asks what those programs mean. Usually a language's meaning is explained in English, in a reference manual, and usually that works well enough. But English is ambiguous, and when two compilers read a manual differently the same program can behave differently on each. Formal semantics gives a precise, mathematical account of meaning. It lets language designers find holes in their designs, lets implementers check their work, and lets anyone prove properties of programs. This lesson introduces the three classic styles, operational, denotational and axiomatic, using a tiny imperative language and Python implementations of each.

You met one piece of this already. CMPUT-272 lesson 12 used preconditions, postconditions and loop invariants to prove small programs correct; that is axiomatic semantics, which we revisit briefly at the end. Here we concentrate on operational semantics, which describes meaning by how programs run, because it maps most directly onto interpreters, the main artifact of this course.

Why formal semantics matters

Informal definitions leave gaps, and gaps cost money. The C standard lists over two hundred situations that are 'undefined behavior', such as signed integer overflow or reading an uninitialized variable. Compilers are allowed to assume these never happen, and modern optimizers use that freedom aggressively, so a program with a hidden overflow may work in a debug build and fail mysteriously when optimized. JavaScript's early specification left the order of object property enumeration unspecified, and websites came to depend on one browser's order. Formal semantics forces every case to be decided.

Some languages have taken the formal route seriously. The Definition of Standard ML (1990, revised 1997) gives the whole language, static and dynamic semantics, as inference rules on a little over a hundred pages. WebAssembly, the low-level language that runs in web browsers, has a formal specification that was mechanized in the Isabelle proof assistant, and the mechanization found errors in the draft. The CompCert C compiler, written and proved correct in the Coq proof assistant, comes with a theorem that the compiled code behaves as the semantics of the source says. These are the strongest guarantees software has ever had.

A small language: IMP

To study semantics we need a language small enough to define completely. IMP, a standard teaching language, has arithmetic expressions (numbers, variables, +, -, *), Boolean expressions (true, false, <=, not, and) and commands: skip (do nothing), assignment x := a, sequencing c1; c2, conditionals if b then c1 else c2, and loops while b do c. A state maps each variable to an integer. The meaning of a command, informally, is how it changes the state. Despite its size, IMP is Turing-complete, so everything interesting about termination and loops already shows up.

Big-step operational semantics

Big-step semantics, also called natural semantics, defines a judgment written ⟨c, s⟩ ⇓ s′, read 'command c, started in state s, terminates in state s′'. The judgment is defined by inference rules. Each rule has premises above a line and a conclusion below it; if all premises hold, the conclusion holds. Rules with no premises are axioms. Here are the rules for assignment, sequencing and the two cases of while:

Here \(\mathcal{A}[\![a]\!]s\) is the value of arithmetic expression a in state s, and \(s[x \mapsto v]\) is the state s updated so that x maps to v. The second while rule is recursive: to know where the loop ends up, run the body once and then run the whole loop again from the new state. If the loop never terminates, there is simply no finite derivation, so no final state is defined. A Python function that follows these rules case by case is a big-step interpreter, and it reads almost exactly like the rules.

# IMP: a tiny imperative language, given a big-step (natural) semantics as a Python function.
# Abstract syntax as tuples:
#   a ::= n | x | ("+", a, a) | ("-", a, a) | ("*", a, a)
#   b ::= True | False | ("<=", a, a) | ("not", b) | ("and", b, b)
#   c ::= ("skip",) | (":=", x, a) | ("seq", c, c) | ("if", b, c, c) | ("while", b, c)
def A(a, s):
    if isinstance(a, int): return a
    if isinstance(a, str): return s[a]
    op, l, r = a
    return {"+": A(l, s) + A(r, s), "-": A(l, s) - A(r, s), "*": A(l, s) * A(r, s)}[op]

def B(b, s):
    if isinstance(b, bool): return b
    if b[0] == "<=": return A(b[1], s) <= A(b[2], s)
    if b[0] == "not": return not B(b[1], s)
    if b[0] == "and": return B(b[1], s) and B(b[2], s)

def C(c, s):
    """Big-step judgement <c, s> => s'.  Returns the final state (a new dict)."""
    tag = c[0]
    if tag == "skip": return s
    if tag == ":=":   return {**s, c[1]: A(c[2], s)}
    if tag == "seq":  return C(c[2], C(c[1], s))
    if tag == "if":   return C(c[2], s) if B(c[1], s) else C(c[3], s)
    if tag == "while":
        return C(c, C(c[2], s)) if B(c[1], s) else s

# factorial:  y := 1; while not (x <= 0) do (y := y * x; x := x - 1)
FACT = ("seq", (":=", "y", 1),
        ("while", ("not", ("<=", "x", 0)),
                  ("seq", (":=", "y", ("*", "y", "x")), (":=", "x", ("-", "x", 1)))))
for n in (0, 1, 5, 10):
    print(f"x = {n:2}:", C(FACT, {"x": n}))

x =  0: {'x': 0, 'y': 1}
x =  1: {'x': 0, 'y': 1}
x =  5: {'x': 0, 'y': 120}
x = 10: {'x': 0, 'y': 3628800}

The structure of a big-step derivation is a tree, and the tree is a proof. A whole family of proofs about programs works by induction on the height of such derivation trees, using the structural induction you learned in CMPUT-272. One standard result is determinism: if ⟨c, s⟩ ⇓ s1 and ⟨c, s⟩ ⇓ s2 then s1 = s2. IMP is deterministic; a language with a nondeterministic choice operator or with threads would not be.

Small-step operational semantics

Big-step semantics only talks about programs that finish. It says nothing about an infinite loop beyond 'no derivation exists', and it cannot describe the interleaving of threads or the moment a program crashes halfway through. Small-step semantics, also called structural operational semantics after Gordon Plotkin's 1981 notes, describes computation as a sequence of single steps: ⟨c, s⟩ → ⟨c′, s′⟩, where c′ is what remains to be done. A program terminates when it reaches skip; it loops when the sequence of steps goes on forever.

The while rule is especially neat: a loop takes one step by unfolding itself into an if whose then branch runs the body and then the loop again. A small-step interpreter applies step repeatedly and can print every configuration along the way, which makes it a useful debugging and teaching tool.

# Small-step (structural operational) semantics for IMP: one step at a time.
def A(a, s):
    if isinstance(a, int): return a
    if isinstance(a, str): return s[a]
    op, l, r = a
    return {"+": A(l, s) + A(r, s), "-": A(l, s) - A(r, s), "*": A(l, s) * A(r, s)}[op]
def B(b, s):
    if isinstance(b, bool): return b
    if b[0] == "<=": return A(b[1], s) <= A(b[2], s)
    if b[0] == "not": return not B(b[1], s)

def step(c, s):
    """One transition <c, s> -> <c', s'>.  ("skip",) is the finished command."""
    tag = c[0]
    if tag == ":=":
        return ("skip",), {**s, c[1]: A(c[2], s)}
    if tag == "seq":
        if c[1] == ("skip",):
            return c[2], s                                   # skip; c2  ->  c2
        c1, s1 = step(c[1], s)
        return ("seq", c1, c[2]), s1                         # step inside the left part
    if tag == "if":
        return (c[2] if B(c[1], s) else c[3]), s
    if tag == "while":                                       # unfold the loop once
        return ("if", c[1], ("seq", c[2], c), ("skip",)), s

def show(c):
    tag = c[0]
    if tag == "skip": return "skip"
    if tag == ":=": return f"{c[1]} := {c[2]}"
    if tag == "seq": return f"{show(c[1])}; {show(c[2])}"
    if tag == "if": return f"if {c[1]} then .. else .."
    if tag == "while": return "while .."

# x := 2; while not (x <= 0) do x := x - 1
prog = ("seq", (":=", "x", 2), ("while", ("not", ("<=", "x", 0)), (":=", "x", ("-", "x", 1))))
c, s, n = prog, {}, 0
while c != ("skip",):
    print(f"{n:2}  {show(c)[:46]:46}  {s}")
    c, s = step(c, s); n += 1
print(f"{n:2}  skip{'':42}  {s}")

 0  x := 2; while ..                                {}
 1  skip; while ..                                  {'x': 2}
 2  while ..                                        {'x': 2}
 3  if ('not', ('<=', 'x', 0)) then .. else ..      {'x': 2}
 4  x := ('-', 'x', 1); while ..                    {'x': 2}
 5  skip; while ..                                  {'x': 1}
 6  while ..                                        {'x': 1}
 7  if ('not', ('<=', 'x', 0)) then .. else ..      {'x': 1}
 8  x := ('-', 'x', 1); while ..                    {'x': 1}
 9  skip; while ..                                  {'x': 0}
10  while ..                                        {'x': 0}
11  if ('not', ('<=', 'x', 0)) then .. else ..      {'x': 0}
12  skip                                            {'x': 0}

Small-step semantics is what abstract machines and debuggers implement, and it is the natural setting for concurrency: to model two threads, let either thread take the next step, and the set of all possible interleavings falls out of the rules. It is also the style used to state type soundness, which lesson 7 proves in the form 'a well-typed program never gets stuck'.

If we define a language twice, the definitions had better agree. For IMP one can prove that ⟨c, s⟩ ⇓ s′ exactly when ⟨c, s⟩ →* ⟨skip, s′⟩, where →* means zero or more steps. The proof is by induction, but we can at least test the claim. The program below generates thousands of random loop-free programs and compares the two interpreters; this kind of differential testing is how real language implementers catch bugs, and it is the core idea behind tools such as Csmith, which found hundreds of bugs in GCC and LLVM by comparing compilers on random C programs.

# The two semantics should agree.  Test that on many random small programs (seeded).
import random
rnd = random.Random(3)

def A(a, s):
    if isinstance(a, int): return a
    if isinstance(a, str): return s[a]
    op, l, r = a
    return {"+": A(l, s) + A(r, s), "-": A(l, s) - A(r, s)}[op]
def big(c, s):
    t = c[0]
    if t == "skip": return s
    if t == ":=": return {**s, c[1]: A(c[2], s)}
    if t == "seq": return big(c[2], big(c[1], s))
    if t == "if": return big(c[2] if A(c[1], s) > 0 else c[3], s)
def step(c, s):
    t = c[0]
    if t == ":=": return ("skip",), {**s, c[1]: A(c[2], s)}
    if t == "seq":
        if c[1] == ("skip",): return c[2], s
        c1, s1 = step(c[1], s); return ("seq", c1, c[2]), s1
    if t == "if": return (c[2] if A(c[1], s) > 0 else c[3]), s
def small(c, s):
    while c != ("skip",): c, s = step(c, s)
    return s

def rand_a(d):
    if d == 0 or rnd.random() < 0.3: return rnd.choice([rnd.randint(-3, 3), "x", "y"])
    return (rnd.choice("+-"), rand_a(d - 1), rand_a(d - 1))
def rand_c(d):
    k = rnd.random()
    if d == 0 or k < 0.35: return (":=", rnd.choice("xy"), rand_a(2))
    if k < 0.7: return ("seq", rand_c(d - 1), rand_c(d - 1))
    return ("if", rand_a(2), rand_c(d - 1), rand_c(d - 1))

trials = 2000
mismatches = sum(big(c, {"x": 1, "y": 2}) != small(c, {"x": 1, "y": 2})
                 for c in (rand_c(4) for _ in range(trials)))
print(f"{trials} random loop-free programs, mismatches between big-step and small-step: {mismatches}")

2000 random loop-free programs, mismatches between big-step and small-step: 0

Denotational semantics

Denotational semantics, pioneered by Christopher Strachey and Dana Scott around 1970, takes a different view. It assigns to each phrase a mathematical object, its denotation, and requires the denotation of a compound phrase to be built only from the denotations of its parts. This requirement is called compositionality. The denotation of an arithmetic expression is a function from states to integers; the denotation of a command is a partial function from states to states, undefined on states where the command loops forever. The double square brackets in \(\mathcal{C}[\![c]\!]\) are the traditional notation for 'the meaning of c'.

Most cases are easy: \(\mathcal{C}[\![c_1; c_2]\!]\) is the composition of the two state transformers. The difficult case is while, because its meaning refers to itself. The solution is to define the meaning of the loop as the least fixed point of a functional F, where F(g) runs the body once and then behaves like g. Starting from the everywhere-undefined function, F applied once gives the meaning of the loop for states that need zero iterations, F applied twice handles up to one iteration, and so on. The loop's meaning is the limit of this chain of approximations. The program below computes the approximations for a summing loop.

# Denotational semantics: the meaning of a while loop is the least fixed point of a functional.
# A state transformer is a partial function from states to states; we represent it as a
# Python function returning None for "undefined" (does not terminate within this approximation).
def F(prev):
    """One unfolding of:  while x > 0 do (y := y + x; x := x - 1)"""
    def meaning(s):
        if s["x"] > 0:
            t = {"x": s["x"] - 1, "y": s["y"] + s["x"]}
            return prev(t)
        return s
    return meaning

bottom = lambda s: None          # the everywhere-undefined function
approx = bottom
start = {"x": 4, "y": 0}
for k in range(7):
    print(f"F^{k}(bottom) applied to {start}: {approx(start)}")
    approx = F(approx)

F^0(bottom) applied to {'x': 4, 'y': 0}: None
F^1(bottom) applied to {'x': 4, 'y': 0}: None
F^2(bottom) applied to {'x': 4, 'y': 0}: None
F^3(bottom) applied to {'x': 4, 'y': 0}: None
F^4(bottom) applied to {'x': 4, 'y': 0}: None
F^5(bottom) applied to {'x': 4, 'y': 0}: {'x': 0, 'y': 10}
F^6(bottom) applied to {'x': 4, 'y': 0}: {'x': 0, 'y': 10}

After five unfoldings the approximation is defined on the state x = 4, because that state needs four iterations, and further unfoldings do not change the answer. Making this idea rigorous for all programs requires domain theory, which Scott developed for exactly this purpose. The pay-off of denotational semantics is equational reasoning: two programs are equivalent if their denotations are equal, and because meanings are compositional, equivalent parts can be swapped inside any larger program. Optimizing compilers rely on such equivalences every time they replace x * 2 with x + x or move a computation out of a loop.

Axiomatic semantics in brief

Axiomatic semantics, introduced by Tony Hoare in 1969 building on Robert Floyd's work, defines a language by what can be proved about its programs. A Hoare triple {P} c {Q} states that if precondition P holds before c runs and c terminates, then postcondition Q holds afterwards. Each construct has a proof rule; the rule for while needs a loop invariant, a property that holds before the loop and is preserved by each iteration. Tools such as Dafny, Frama-C and SPARK Ada build on this idea to verify real software, and Amazon Web Services uses related techniques to check parts of its storage and identity systems.

# Hoare logic: {P} c {Q}.  We cannot prove a triple by testing, but we can look for
# counterexamples quickly.  Check the loop invariant for summing 1..n.
import random
rnd = random.Random(7)

def run(n, check):
    i, total = 0, 0
    assert check(i, total, n), "invariant fails on entry"
    while i < n:
        i, total = i + 1, total + i + 1
        assert check(i, total, n), f"invariant fails after i={i}"
    return total

good = lambda i, t, n: t == i * (i + 1) // 2 and i <= n
bad  = lambda i, t, n: t == i * i                     # a wrong guess at an invariant

for name, inv in (("total = i(i+1)/2 and i <= n", good), ("total = i*i", bad)):
    try:
        for _ in range(500):
            n = rnd.randint(0, 50)
            assert run(n, inv) == n * (n + 1) // 2
        print(f"{name:30} survived 500 random tests")
    except AssertionError as e:
        print(f"{name:30} refuted: {e}")

total = i(i+1)/2 and i <= n    survived 500 random tests
total = i*i                    refuted: invariant fails after i=2

Worked examples