Programming language semantics

The meaning of constructs in a programming language, including their permitted values and execution behavior. Programming language syntax organizes constructs; a type system and execution rules give further constraints and meaning.

A mapping from identifiers to their semantic values. A programming closure retains its defining semantic environment; extending it for parameters preserves lexical scope and lets those parameters shadow outer bindings.

A representation of the rest of a computation. In continuation-passing style, a computation receives a function telling it how to use its result. An explicit computer memory argument can be supplied when the continuation is invoked, so capturing control need not capture a snapshot of computer memory.

A computation that can suspend and later resume. A first-class continuation can represent its suspended control state while mutable computer memory remains shared.

Tasks transfer control at explicit suspension points. A FIFO queue of runnable continuations implements round-robin scheduling; a task that never transfers control can prevent others from running.

A continuation represented as an ordinary language value that can be stored and later invoked. Whether it may be invoked once or repeatedly, and whether mutable program state is restored, are separate semantic choices.

Supply the current continuation to a user function. A language can expose this as an escape function or as a separate continuation value with its own invocation primitive; those interfaces need corresponding semantic definitions.

Pass the remaining computation explicitly as a continuation. Returning a value means invoking that continuation; a different control destination can be selected by invoking a different continuation.

A variable used within a procedure but declared outside it. Under lexical scope, its binding is determined by enclosing declarations and the associated runtime environment, often accessed through a static chain or programming closure.

Name resolution determined by the nesting of declarations in the source program. An activation of a nested procedure obtains its nonlocal variables from its defining environment, which can differ from the newest activation of the same enclosing procedure when procedural parameters are used.

A suspended computation together with the information needed to evaluate it later. In lazy evaluation by need, forcing a thunk computes and records its result, so subsequent demands can reuse it. Deferral and memoization are distinct: a merely delayed computation need not share its result unless its evaluation mechanism provides that sharing.

The convention relating a procedure's formal parameters to its arguments. Copying a large array at every recursive call can dominate running time, even when the procedure never modifies the argument.

Evaluate argument expressions before invoking a function. A monadic interpreter must also specify the order of those evaluations when its computational monad represents effects.

A parameter initialized from the actual argument's value. Whether passing an aggregate copies all elements or merely a reference is language-dependent; in whole-array copying semantics, a length-$L$ argument costs $\Theta (L)$ per call. This differs from a language that passes an object reference by value.

A parameter that designates the caller's actual storage, rather than a complete copied value. Read-only algorithms may use reference parameters to avoid copying, while their correctness arguments still prohibit writes. The VAR convention used in Oberon exam pseudocode has this purpose.

Evaluation that skips a later operand once an earlier operand determines the result. In Scala, p != null && p.field == x does not dereference p when it is null, and i < n && a(i) != x avoids an out-of-range access at $i=n$. The order is part of the safety argument: exchanging these operands can preserve a Boolean formula in mathematics while changing whether a program raises an exception.

Evaluation delayed until a result is demanded, with sharing of the delayed computation's result. A lazy list can expose a constructor before computing its tail; this permits productive infinite structures and lazy feedback streams. A non-strict language can implement its semantics this way without making every function non-strict.

Represent a cursor by an underlying consuming iterator plus an optional cached head. Without a cache, its abstract sequence is the iterator's sequence; with cached $v$, it is $[v]$ concatenated with the remaining iterator sequence. current fetches and caches exactly one value when needed, repeated reads reuse it, and advance discards it. Availability testing need not fetch a value, and construction need not query the input. This avoids forcing a future stream element that the client may never request.

An undefined or nonterminating computation in the denotational account of Haskell. A structured value may contain bottom values while retaining a defined outer constructor: undefined : [] is distinguishable from an entirely undefined list.^[ref]

A description of the information needed to determine a program's next permitted step. In the summation loop verification, this includes the current variable values and the position in the instructions.

An integer arithmetic result outside the range of its chosen representation. A programming language may specify wrapping, trapping or another behavior; a proof over mathematical integers must account for that difference.

A system of rules for proving Hoare triples by following a program's structure. Variable assignment, sequential composition and loops have corresponding proof obligations.

A partial correctness claim connecting a precondition $P$, a program $C$ and a postcondition $Q$: every terminating execution begun with $P$ ends with $Q$. State separately whether total correctness is intended.