VU-VFS-2025. Lecture 5 - Nano & Hoare Logic [003s]

  • December 4, 2025

1. Simple Imperative Language Syntax & Semantics

  • December 4, 2025

Definition 1.1. Simple Imperative Language - Syntax [003t]

  • December 4, 2025

We define the syntax of a simple imperative programming language, using the followng bnf grammar:

Definition 1.2. Simple Imperative Language - Semantics [003u]

  • December 4, 2025

We can divide the environmental big-step semantics of our simple language into three parts:

  • Expression evaluation: Describes how arithmetic expressions are evaluated to numbers.
  • Boolean expression evaluation: Describes how boolean expressions are evaluated to boolean values (true/false).
  • Statement execution: Describes how statements are executed, transforming an initial state (environment) into a final state.

The general big-step environmental evalutation rule is denoted as:

\[ \langle t, \sigma \rangle \Downarrow v \]

Here:

  1. We have some starting term \(\texttt {t}\) (which can be an expression, boolean expression, or statement), along with some state \(\sigma \).
  2. The evaluation results in some value \(\texttt {v}\) (which can be a number, boolean value, or new state).

A quick aside here to deconstruct the term big-step environmental evaluation:

  • We say that this evaluation is big-step as it assumes some arbitrary state of intermediate steps, meaning that within big step semantics we do not care about intermediate computation only about some input expression and the final output value. A simple analogue to make here is that big-step semantics are akin to a teacher asking you to only show ur final answer to a math problem rather than all the steps you took to get there.
  • We say that this evaluation is environmental (as opposed to being substitution based) as we explicitly keep track of a state \(\sigma \) which maps variables to their values. This is in contrast to substitution based semantics where variable occurrences are replaced directly with their values in expressions.

The state \(\sigma : \texttt {String} \to \mathbb {Z}\) represents a mapping from variables (commonly strings) to their corresponding values (numbers). We denote the updated state after assigning a value to a variable \(\texttt {x}\) as:

\[ \sigma [x \mapsto n] \]

This means that in the new state, the variable \(\texttt {x}\) now maps to the number \(\texttt {n}\), while all other variable mappings remain unchanged from the original state \(\sigma \).

1.2.1. Expression evaluation

  • December 4, 2025

1.2.2. Boolean expression evaluation

  • December 4, 2025

1.2.3. Statement evaluation

  • December 4, 2025

Quiz 1.3. Simple Imperative Language - Evaluation [003v]

  • December 4, 2025
  1. What does the following evaluate to? \[ \langle (x := x - 1), \sigma [x \mapsto 2] \rangle \]
  2. What does the following evaluate to? \[ \langle \texttt {if } x + 1 \leq 3 \texttt { then } x := x - 1, \sigma [x \mapsto 1] \rangle \]
  3. What does the following evaluate to? \[ \langle \texttt {while } (x + 1 \leq 3) \texttt { then } x := x - 1, \sigma [x \mapsto 1] \rangle \]
  4. Is the following a total function? \[ \langle e, \sigma \rangle \Downarrow n \]
  5. Is the following a total function? \[ \langle s, \sigma \rangle \Downarrow \sigma ' \]

Solution. 

  • December 4, 2025
  1. Starting in the state \(x \mapsto 2\) we evaluate \(x := x - 1\) to the state \(x \mapsto 1\)
  2. Starting in the state \(x \mapsto 1\), we first evaluate the condition \(x + 1 \leq 3\): \[ \begin {align*} \langle x + 1, \sigma [x \mapsto 1] \rangle &\Downarrow 2 \\ \langle 3, \sigma [x \mapsto 1] \rangle &\Downarrow 3 \\ \langle 2 \leq 3, \sigma [x \mapsto 1] \rangle &\Downarrow \texttt {true} \end {align*} \] Since the condition evaluates to true, we then evaluate the then-branch \(x := x - 1\): \[ \begin {align*} \langle x - 1, \sigma [x \mapsto 1] \rangle &\Downarrow 0 \\ \langle x := 0, \sigma [x \mapsto 1] \rangle &\Downarrow \sigma [x \mapsto 0] \end {align*} \]
  3. We again start by evaluating the condition \[ \begin {align*} \langle x + 1, \sigma [x \mapsto 1] \rangle &\Downarrow 2 \\ \langle 3, \sigma [x \mapsto 1] \rangle &\Downarrow 3 \\ \langle 2 \leq 3, \sigma [x \mapsto 1] \rangle &\Downarrow \texttt {true} \end {align*} \] Since we can see that the body of the loop only decreases \(x\), we are stuck in an infinite loop: \[ \begin {align*} \langle x := x - 1, \sigma [x \mapsto 1] \rangle &\Downarrow \sigma [x \mapsto 0] \\ \langle \texttt {while } (x + 1 \leq 3) \texttt { do } x := x - 1, \sigma [x \mapsto 0] \rangle &\Downarrow \sigma [x \mapsto -1] \\ \langle \texttt {while } (x + 1 \leq 3) \texttt { do } x := x - 1, \sigma [x \mapsto -1] \rangle &\Downarrow \sigma [x \mapsto -2] \\ &\vdots \end {align*} \]
  4. Yes, for every expression \(e\) and state \(\sigma \), there exists a number \(n\) such that \[ \langle e, \sigma \rangle \Downarrow n \] This follows from the fact that expressions are finite syntax trees built from a finite set of rules, and each rule can be evaluated in a finite number of steps.
  5. No, there exist statements \(s\) and states \(\sigma \) for which there is no resulting state \(\sigma '\) such that \[ \langle s, \sigma \rangle \Downarrow \sigma ' \] For example, consider the while-loop \[ \texttt {while } (x + 1 \leq 3) \texttt { do } x := x - 1 \] starting from the state \(\sigma [x \mapsto 1]\). As shown in the previous question, this loop does not terminate, and thus there is no resulting state \(\sigma '\).