L07 - Relational Semantics

Back to Program Verification Index | Previous: (y-06) Boogie and Boostan | Next: (y-08) Hoare Proof System

Mental Model for Relational Semantics

• Programs as Relations: In verification, we don’t just “run” code; we view a statement as a Binary Relation between the state before and the state after.
• State: A mapping from every program variable to a value (e.g., $\{a\to 5,b\to 10\}$).
• Composition: Running two statements in a row is mathematically represented as the Relational Composition of their individual relations.
• Loops: A while loop is represented as the Reflexive Transitive Closure ($R^{\ast }$) of its body, filtered by the exit condition.

What is a Program State?

A Program State $s$ is a function that assigns a value to every variable in the program.

• If we have variables $V=\{a,b\}$, a state might be $s=\{a\mapsto 23,b\mapsto 42\}$.
• We use FOL formulas to describe sets of states. For example, the formula $a>0\wedge b=0$ represents all possible states where $a$ is positive and $b$ is zero.

---

Relational Semantics of Boostan

We define the meaning (semantics) of each Boostan statement $[[\text{stmt}]]$ as a relation $R\subseteq \text{State}\times \text{State}$.

1. Assignment: x := expr

The relation consists of pairs $(s,s^{\prime })$ where:

• The new value of $x$ (in $s^{\prime }$) is the result of evaluating expr in the old state $s$.
• All other variables $v\ne x$ remain unchanged ($s^{\prime }(v)=s(v)$).

Formal Definition: $[[x:=e]]=\{(s,s^{\prime })\mid s^{\prime }(x)=[[e]{]}_s\text{ and }\forall v\ne x,s^{\prime }(v)=s(v)\}$

2. Composition: st1; st2

Running st1 followed by st2 is the relational composition: $[[st1]]\circ [[st2]]$.

• $(s,s^{\prime \prime })$ is in the relation if there exists an intermediate state $s^{\prime }$ that links them.

Formal Definition: $[[s{t}_1;s{t}_2]]=[[s{t}_1]]\circ [[s{t}_2]]=\{(s,s^{\prime \prime })\mid \exists s^{\prime },(s,s^{\prime })\in [[s{t}_1]]\text{ and }(s^{\prime },s^{\prime \prime })\in [[s{t}_2]]\}$

3. If-Then-Else: if (B) {st1} else {st2}

The relation follows one of two branches based on the Boolean condition $B$.

Formal Definition: $[[\text{if }B\{s{t}_1\}\text{else }\{s{t}_2\}]]=(\{B\}\times \text{State}\cap [[s{t}_1]])\cup (\{\neg B\}\times \text{State}\cap [[s{t}_2]])$

---

Semantics of Loops: while (B) {st}

Loops are the most complex part of relational semantics. We use the Reflexive Transitive Closure ($R^{\ast }$) to model an arbitrary number of iterations (0 or more).

1. Let $R_{body}$ be the relation of the loop body given that $B$ is true: $R_{body}=\{(s,s^{\prime })\mid s\in \{B\}\text{ and }(s,s^{\prime })\in [[st]]\}$.
2. The loop execution is $R_{body}^{\ast }$. This represents “running the body $n$ times.”
3. The final state must satisfy $\neg B$ (the loop must have terminated).

Formal Definition: $[[\text{while }B\{st\}]]=(\{(s,s^{\prime })\mid s\in \{B\}\text{ and }(s,s^{\prime })\in [[st]]\}{)}^{\ast }\circ \{(s,s)\mid s\in \{\neg B\}\}$ Equivalently: $[[\text{while }B\{st\}]]=R_{body}^{\ast }\cap (\text{State}\times \{\neg B\})$

---

Precondition-Postcondition Pairs

We say a program is correct with respect to a precondition ${\varphi }_{\text{pre}}$ and a postcondition ${\varphi }_{\text{post}}$ if the set of all possible final states is contained within the postcondition.

Formal Definition: $\text{post}(\{{\varphi }_{\text{pre}}\},[[st]])\subseteq \{{\varphi }_{\text{post}}\}$ Where $\text{post}(Y,R)=\{s^{\prime }\mid \exists s\in Y,(s,s^{\prime })\in R\}$.

---

Summary

1. State: Mapping from variables to values.
2. Statements as Relations: Mapping from “State Before” to “State After”.
3. Composition: Sequence of statements = mathematical composition of relations.
4. While Loops: Use reflexive transitive closure ($R^{\ast }$) to model arbitrary iterations.
5. Correctness: The set of reachable final states must be a subset of the desired postcondition.

Self-Check

1. Why does relational semantics view a statement as a binary relation rather than a function?

Answer

A function takes one input state to one output state, which does not handle non-determinism (havoc) or filtering (assume). A binary relation $R\subseteq \text{State}\times \text{State}$ allows a state to be related to several successors (non-determinism) or to none at all (a blocked path). This matches Boostan’s actual behavior.

2. Give the relation $[[x:=e]]$ in words.

Answer

The pair $(s,s^{\prime })$ is in $[[x:=e]]$ iff $s^{\prime }(x)$ equals the value of $e$ evaluated in $s$, and $s^{\prime }$ agrees with $s$ on every other variable. Assignment changes exactly the assigned variable and leaves the rest of the state untouched.

3. How is sequencing $s{t}_1;s{t}_2$ defined in relational semantics, and what does the intermediate state mean?

Answer

$[[s{t}_1;s{t}_2]]=[[s{t}_1]]\circ [[s{t}_2]]=\{(s,s^{\prime \prime })\mid \exists s^{\prime }.(s,s^{\prime })\in [[s{t}_1]]\wedge (s^{\prime },s^{\prime \prime })\in [[s{t}_2]]\}$. The intermediate state $s^{\prime }$ is the state after $s{t}_1$ runs and before $s{t}_2$ runs; sequencing is exactly relational composition.

4. Why does the semantics of while (B) {st} use the reflexive transitive closure $R^{\ast }$?

Answer

A loop may execute its body zero, one, or arbitrarily many times before $B$ becomes false. $R^{\ast }$ is the smallest relation containing all finite iterations of $R$ plus the identity (zero iterations). Intersecting with $\text{State}\times \{\neg B\}$ keeps only those final states where the loop guard has become false, i.e., the loop actually terminated.

5. What does $\text{post}(\{{\varphi }_{\text{pre}}\},[[st]])\subseteq \{{\varphi }_{\text{post}}\}$ say about partial correctness?

Answer

For every initial state satisfying ${\varphi }_{\text{pre}}$, every state reachable through $[[st]]$ satisfies ${\varphi }_{\text{post}}$. It is partial because the inclusion is vacuous when $st$ has no terminating execution from $s$: the relation simply contains no pair starting at $s$. Total correctness would additionally require termination.

---

Back to Program Verification Index | Previous: (y-06) Boogie and Boostan | Next: (y-08) Hoare Proof System | (y) Return to Notes | (y) Return to Home