A small-step operational semantics defines program execution as a sequence of elementary state transitions.

A judgment

$$e\to e'$$

means that expression $e$ performs one computation step and becomes $e'$. Rules specify the allowed steps. For arithmetic, for example,

$$\frac{e_1\to e_1'}{e_1+e_2\to e_1'+e_2}$$

says that the left operand may take a step inside an addition. Once both operands are numeric values, a rule performs the arithmetic itself.

If

$$e_0\to e_1\to e_2\to\cdots\to v,$$

then repeated small steps describe the full execution ending at value $v$. An infinite sequence models divergence; a non-value with no applicable rule is stuck.

Small-step semantics exposes evaluation order and intermediate states, making it especially useful for concurrency, exceptions, control flow and proofs such as type safety. Rather than describing how an implementation happens to run, it gives an abstract machine-independent definition of what one step of the language means.