Skip to main content

Section D.14 Exercise Sheet 14

Hoare (copied from last sheet)

1. Hoare Logic.

Use the rules for Hoare triples to derive a valid precondition \(P\text{.}\)

  1. \(\displaystyle \vdash\hoare{P}{\texttt{a = a + 2;}}{a == 42}\)

  2. \(\displaystyle \vdash\hoare{P}{\texttt{\{ a = b * c; b = c + a; c = c - 17; \}}}{\texttt{a == b} \land \texttt{b == c + 59}}\)

  3. \(\displaystyle \vdash\hoare{P}{\texttt{if (a == 0) abort(); else x = x + 1;}}{x > 0}\)

  4. \(\displaystyle \vdash\hoare{P}{\texttt{if (x < 0) y = -x; else y = x;}}{\texttt{y > 0} \land \texttt{X * X == y * y}}\)

  5. \(\displaystyle \vdash\hoare{P}{\texttt{x = x / z;}}{\texttt{x != 0} \land \texttt{z == 0}}\)

202207281550

202207151400
Solution.
  1. Using [Assign], we can derive: \(P = (a == 42)[a + 2 / a] = (a + 2 == 42) \Leftrightarrow (a == 40)\)

  2. \(\displaystyle P = (b * c == c + b * c \land c + b * c == c - 17 + 59) \Leftrightarrow (c == 0 \land b * c == 42) \Leftrightarrow \mathit{false}\)

  3. \(\displaystyle P = (\texttt{a == 0} \land \mathit{false}) \lor (\texttt{a != 0} \land \texttt{x + 1 > 0}) \Leftrightarrow (\texttt{a != 0} \land \texttt{x > -1})\)

  4. \(\displaystyle P = ((x < 0 \land (-x) > 0 \land X * X == (-x) * (-x)) \lor (\neg (x < 0) \land \texttt{x > 0} \land \texttt{X * X == x * x})) \Leftrightarrow (\texttt{x != 0} \land \texttt{X * X == x * x})\)

  5. \(\displaystyle P = (\texttt{z != 0} \land (\texttt{x / z != 0} \land \texttt{z == 0})) \Leftrightarrow \mathit{false}\)

2. Hoare Logic: Assignments.

Find a valid precondition \(P\) for the following Hoare triples.

  1. \(\displaystyle \vdash\hoare{P}{\texttt{x = x - 1;}}{x == 5}\)

  2. \(\displaystyle \vdash\hoare{P}{\texttt{x = 7;}}{x == 5}\)

  3. \(\displaystyle \vdash\hoare{P}{\texttt{x = 7;}}{x == 7}\)

  4. \(\displaystyle \vdash\hoare{P}{\texttt{a = a - b;}}{a > b}\)

202207281550

202207151400
Solution.

Using the rule Assign, we can derive the following preconditions:

  1. \(\displaystyle P = (x == 5)[x - 1 / x] = (x - 1 == 5) \Leftrightarrow (x == 6)\)

  2. \(\displaystyle P = (x == 5)[7 / x] = (7 == 5) \Leftrightarrow \mathit{false}\)

  3. \(\displaystyle P = (x == 7)[7 / x] = (7 == 7) \Leftrightarrow \mathit{true}\)

  4. \(\displaystyle P = (a > b)[a - b / a] = (a - b > b) \Leftrightarrow (a > 2b)\)

3. Trivial State Sets.

Which sets of states are described by the assertions \(\mathit{true}\) and \(\mathit{false}\text{?}\)

202207281550

202207151400
Solution.

The assertion \(\mathit{true}\) describes the set of all states, i.e. \(\Sigma\text{.}\) The assertion \(\mathit{false}\) describes the empty set \(\emptyset\text{.}\)

4. Comparison.

{
    q = 0;
    while (x >= y) {
        q = q + 1;
        x = x - y;
    }
    r = x;
}
C0 program for division. \(r\) contains the remainder of the division and \(q\) the quotient.
let div x y = 
  if x < y then 
    (1,x) 
  else 
    let (q,r) = div (x-y) y in 
    (q+1,r)
OCaml program for division.

\begin{equation*} div(x,y):=\begin{cases} (0,x) & (x \lt y) \\ (q+1,r) & (x \geq y), (q,r) = div(x-y, y) \\ \end{cases} \end{equation*}

Recursive function for division.

Prove for the OCaml program / the mathematical definition of div the specification \(0\leq x \land y > 0 \to q\cdot y + r = x \land 0\leq r \lt y\text{.}\)

Compare your proof to the correctness proof of the C0 program done using hoare logic. What are the similarities and differences?

202207281550

202207151400
Solution.

{
    // {x = X & 0 <= x [2]}
    q = 0;
    // {q*y + x = X [3] & 0 <= x}
    while (x >= y) {
        // {q*y + x = X & 0 <= x & x >= y}
        // {q*y + x + y - y = X [b] & 0 <= x-y [a]}
        q = q + 1;
        // {q*y + x - y = X [b] & 0 <= x-y}
        x = x - y;
    // {q*y + x = X & 0 <= x}
    }
    // {q*y + x = X & 0 <= [2] x < y [1,c]}
    r = x;
    // {q*y + r = X & 0 <= r < y}
}
The C0 program annotated with its correctness proof as performed using hoare logic. The numbers and letters in brackets show the correspondence to the induction proof.

In hoare logic, the case for \(y\lt 0\) is not considered as the program diverges. Nevertheless, the post-condition is able to prove \(0\lt y\text{.}\)

Proof by complete induction on \(x\text{.}\)

\begin{equation*} \text{IH: }\forall x'\lt x.~x'>0\to \forall m'~r'.~(m',r') = div~x'~y' \to m'y+r'=x' \land 0\leq r'\lt y \end{equation*}

Case distinction on \(x\geq y\text{.}\)

Case \(x\lt y\text{.}\) To show:

\begin{equation*} \begin{array}{cl} 0\cdot y + x = x &(I) \\ 0\leq x \lt y &(II) \end{array} \end{equation*}

(I) follows by reflexivity of equality and corresponds to [3]. The first inequality of (II) follows by assumption and corresponds to [2]. The second part is a consequence of the current case distinction and corresponds to [1].

Case \(x\geq y\text{.}\) To show:

\begin{equation*} \begin{array}{cl} m'\cdot y + r' + y = x &(I) \\ 0\leq r' \geq y &(II) \end{array} \end{equation*}

for \((m',r') = div~(x-y)~y\text{.}\) We have \(x'=x-y > 0\) from \(x\geq y\) (current case). This step corresponds to [a]. To apply the induction hypothesis, \(x'=x-y \lt x\) is needed which follows from the assumption \(y>0\text{.}\) We get:

\begin{equation*} \begin{array}{cl} m'\cdot y + r' = x-y &(IH_I) \\ 0\leq r' \geq y &(IH_{II}) \end{array} \end{equation*}

(II) is a direct consequence of \((IH_{II})\) and corresponds to [c]. (I) follows from \((IH_I)\) using arithmetic and corresponds to [b].

5. Programs.

Give programs that make the following Hoare triples valid for any Q.

  1. \(\displaystyle \vdash\hoare{Q}{?}{\lfalse}\)

  2. \(\displaystyle \vdash\hoare{Q}{?}{\ltrue}\)

  3. \(\displaystyle \vdash\hoare{\lfalse}{?}{Q}\)

  4. \(\displaystyle \vdash\hoare{\ltrue}{?}{Q}\)

202207281550

202207151400
Solution.
  1. \begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare{Q\land\ltrue}{\{\}}{Q}$} \UnaryInfC{$\vdash\hoare{Q}{\texttt{while ($\ltrue$) \{\}}}{Q\land\neg\ltrue}$} \end{prooftree} \end{equation*}
  2. \begin{equation*} \begin{prooftree} \AxiomC{$Q\simp\ltrue$} \AxiomC{} \UnaryInfC{$\vdash\hoare{\ltrue}{\{\}}{\ltrue}$} \BinaryInfC{$\vdash\hoare{Q}{\{\}}{\ltrue}$} \end{prooftree} \end{equation*}
  3. \begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare{\lfalse}{\texttt{abort();}}{Q}$} \end{prooftree} \end{equation*}
  4. \begin{equation*} \begin{prooftree} \AxiomC{$\lfalse\simp Q$} \AxiomC{} \UnaryInfC{$\vdash\hoare{\ltrue\land\ltrue}{\{\}}{\ltrue}$} \UnaryInfC{$\vdash\hoare{\ltrue}{\texttt{while ($\ltrue$) \{\}}}{\ltrue\land\neg\ltrue}$} \BinaryInfC{$\vdash\hoare{\ltrue}{\texttt{while ($\ltrue$) \{\}}}{Q}$} \end{prooftree} \end{equation*}
6. ReLU.

Verify the following program

d = x - y;
if (d < 0)
    r = 0;
else
    r = d;
against the specification \((P,Q)\)

\begin{equation*} P = \ltrue \qquad Q = \underbrace{(\texttt{x - y < 0} \land \texttt{r = 0})}_{Q_1} \lor \underbrace{(\texttt{x - y >= 0} \land \texttt{r = x - y})}_{Q_2}. \end{equation*}
202207281550

202207151400
Solution.

Let \(R := (\texttt{d == x - y})\text{.}\)

7. Primes.

Consider the following algorithm to detect if a number is a prime or not:

r = 1;
i = 2;
while (i < n)
{                   // \
    if (n % i == 0) //  \
        r = 0;      //   } =: s
    i++;            //  /
}                   // /

Come up with a specification that expresses that the program checks if a number is a prime or not and verify it against that specification.

202207281550

202207151400
Solution.

Let \(R := \texttt{r == 1} \liff\forall x. \texttt{x > 1 $\limp$ x < n $\limp$ n \% x != 0}\text{.}\)

Let \(I := i > 1 \land (\texttt{r == 1} \liff\forall x. \texttt{x > 1 $\limp$ x < i $\limp$ n \% x != 0})\text{.}\)

Let \(I' := i + 1 > 1 \land (\texttt{r == 1} \liff\forall x. \texttt{x > 1 $\limp$ x < i + 1 $\limp$ n \% x != 0})\text{.}\)

Let \(I'' := \texttt{r == 0}\land\texttt{i > 1}\land\texttt{n \% i == 0}\text{.}\) Let \(I''' := \texttt{n \% i == 0}\land \texttt{i > 1}\text{.}\)

8. Soundness of if-then-else.

Sketch a soundness proof for the if-then-else rule. Take the proof sketch for the block rule as a template.

202207281550

202207151400
Solution.

The if-then-else rule is

\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{e\land P}{s_1}{Q}$} \AxiomC{$\vdash\hoare{\neg e\land P}{s_2}{Q}$} \BinaryInfC{$\vdash \hoare{\exprdef e\land P}{\CIf{e}{s_1}{s_2}}{Q} $} \end{prooftree}. \end{equation*}

The induction hypothesis tells us that the Hoare triples in the premises are sound, so we have \(\models\hoare{e\land P}{s_1}{Q}\) and \(\models\hoare{\neg e\land P}{s_2}{Q}\text{.}\)

We need to show that:

\begin{equation*} \forall\sigma.\,(\sigma\models \exprdef e \land P)\limp \left(\forall c.\config{\CIf{e}{s_1}{s_n}}\sigma\bigstep c \limp(\exists \sigma'.\,c=\sigma'\land\sigma'\models Q)\right) \end{equation*}

Let \(\sigma\) be a state such that \(\sigma\models\exprdef e\land P\) and let \(c\) be a configuration such that

\begin{equation*} \config{\CIf{e}{s_1}{s_n}}\sigma\bigstep c \end{equation*}

holds. Because of \(\sigma\models\exprdef e\land P\) we either have \(\sigma\models e\land P\) or \(\sigma\models\neg e\land P\text{.}\) Assume without loss of generality (the other case is analogous) that \(\sigma\models e\land P\text{.}\) By inversion of the big step semantics we know that \(\config{s_1}{\sigma}\bigstep c\text{.}\) If \(c\) is not a state (i.e. \(\config{s_1}{\sigma}\) gets stuck or is aborted), then this would contradict the first induction hypothesis \(\models\hoare{e\land P}{s_1}{Q}\text{.}\) Thus, \(\config{s_1}{\sigma}\) must terminate properly in some state \(\sigma'\) with

\begin{equation*} c = \sigma' \land\sigma'\models Q, \end{equation*}

concluding the proof.

Invariants

9. Finding Invariants.

Take a look at the following loops and the invariants \(I\text{.}\)

  1. \(I = \mathit{true}\)
    x = 10;
    y = 5;
    while (x <= y) {
        y = y - x;
    }
    
  2. \(I = \texttt{x = (B - b) * a}\)
    x = 0;
    b = B;
    while (b > 0) {
        x = x + a;
        b = b - 1;
    }
    
  3. \(I = \texttt{a = x + t}\)
    a = 0;
    while (x > 0) {
        t = x % 10;
        a += t;
        x -= t;
        x /= 10;
    }
    
  • Are the supplied invariants functions valid? Argue shortly.

  • Prove your positive answers using the Hoare logic derivation rules.

  • If the invariants are not valid, find suitable ones and prove their validity using the Hoare derivation rules.

202207281550

202207151400
Solution.

In general, it holds that \(I\) is an invariant if \(\vdash \hoare{I \land e}{\texttt{s}}{I}\text{.}\)

  • \(I\) is the trivial invariant.
  • \(I\) is an invariant since B - b counts the number of loop iterations and x is incremented by a in each iteration.
  • \(I\) is not an invariant, for example if \(a = 0\text{,}\) \(t = -15\text{,}\) \(x = 15\) then after the first loop iteration we have \(a = 5\text{,}\) \(t = 5\) and \(x = 1\text{.}\) If we choose \(I' := \texttt{x >= 0}\) as the loop invariant:

All in one

10. GCD.

Consider the following C0 program that computes the greatest common divisor:

while (a != b)
    if (a > b)     // \
        a = a - b; //  \
    else           //   } =: s
        b = b - a; //  /
  1. Compute the static semantics of this program.

  2. Generate MIPS machine code for it according to the rules of the lecture.

  3. Verify that this program is correct with respect to the specification \((P,Q)\)

    \begin{equation*} P = \texttt{a > 0} \land \texttt{b > 0}\land A == a\land B == b \qquad Q = \texttt{a == }\textit{gcd}(A,B) \end{equation*}

    Hint: Pick an appropriate loop invariant.

202207281550

202207151400
Solution.
  1. Static semantics:

  2. gcd:
        .globl
        subiu $sp $sp 12
        sw    $ra 8($sp)
        sw    $a0 0($sp)
        sw    $a1 4($sp)
    # c_while
        b T
    L:
    # c_if
    # c_binary
    # c_var
        addiu $t0 $sp 0
    # c_LtoR
        lw    $t0 $t0
    # c_var
        addiu $t1 $sp 4
    # c_LtoR
        lw    $t1 $t1
        slt   $t0 $t1 $t0
        beqz  $t0 F
    # c_assign
    # c_binary
    # c_var
        addiu $t0 $sp 0
    # c_LtoR
        lw    $t0 $t0
    # c_var
        addiu $t1 $sp 4
    # c_LtoR
        lw    $t1 $t1
        subu  $t0 $t0 $t1
        sw    $t0 0($sp)
        b N
    F:
    # c_assign
    # c_binary
    # c_var
        addiu $t0 $sp 0
    # c_LtoR
        lw    $t0 $t0
    # c_var
        addiu $t1 $sp 4
    # c_LtoR
        lw    $t1 $t1
        subu  $t1 $t0 $t1
        sw    $t1 4($sp)
    N:
    T:
    # c_binary
    # c_var
        addiu $t0 $sp 0
    # c_LtoR
        lw    $t0 $t0
    # c_var
        addiu $t1 $sp 4
    # c_LtoR
        lw    $t1 $t1
        xor   $t0 $t0 $t1
        bnez  $t0 L
    gcd_end:
    # c_var
        addiu $t0 $sp 0
    # c_LtoR
        lw    $t0 $t0
        addiu $v0 $t0 0
        lw    $ra 8($sp)
        addiu $sp $sp 12
        jr    $ra
    
    Run
  3. Let \(I := \texttt{a > 0 $\land$ b > 0 }\land\textit{gcd}(\texttt{a,b})\texttt{ == }\textit{gcd}(A,B)\text{.}\)

    The remaining proof obligation is (and analogously with a and b swapped):

    \begin{equation*} I\land a > b\simp I[a-b/b]. \end{equation*}

    Let \(a > b > 0\) and let \(x\defeq\textit{gcd}(a,b)\text{.}\) We have to show:

    1. \(\displaystyle a - b > 0\)

    2. \(\displaystyle b > 0\)

    3. \(\displaystyle \textit{gcd}(a-b,b) = x\ (= \textit{gcd}(a,b) = \textit{gcd}(A,B))\)

    The goals (i) and (ii) follow directly from the assumptions.

    By the definition of \(\textit{gcd}\text{,}\) there are \(n,m > 0\) such that \(a = n x\) and \(b = m x\text{,}\) and \(x\) is the greatest natural number with that property. Furthermore, we have \(n > m\) and \(n - m > 0\) and \(a - b = nx - mx = (n-m)x\text{.}\) Thus \(x\) is also a common divisor of \(a-b\) and \(b\text{.}\)

    Assume there is another common divisor \(x' > x\text{.}\) Then there are \(n',m' > 0\) such that:

    \begin{equation*} a-b = n'x' \land b = m'x' \end{equation*}

    But then we would have

    \begin{equation*} a = n'x' + m'x' = (n'+m')x' \end{equation*}

    and \(x'\) would also be a common divisor of \(a\) and \(b\) which is a contradiction to the assumption \(x = \textit{gcd}(a,b)\text{.}\)

    Consequently, \(\textit{gcd}(a-b,b) = x\text{.}\)