Formal methods

Answer key — Formal methods

1. 1.

   (a), (b) and (d). Triple (a) is valid because no run from $x = 1$ terminates — partial correctness is silent about divergence. (b) follows from the assignment axiom. (c) fails on the run $x = 3 \mapsto 4$. (d) follows from the loop rule with invariant $x \ge 0$: $I \wedge \neg(x \gt 0)$ implies $x = 0$; here the loop also terminates, with variant $x$.

2. 2.

   $\mathrm{wp}(z := 2y, z = 20) = (2y = 20)$, and $\mathrm{wp}(y := x + 3, 2y = 20) = (2(x+3) = 20)$, i.e. $x = 7$. So $n = 7$. Assignment works backwards: the last command is substituted first.

3. 3.

   Take $I \equiv s = i(i+1)/2 \wedge i \le n$. (1) Initially $s = i = 0$ and $n \ge 0$. (2) If $I$ and $i \lt n$, then after $i := i+1;\ s := s + i$ the new values satisfy $s' = i(i+1)/2 + (i+1) = (i+1)(i+2)/2$ and $i' = i + 1 \le n$. (3) $I \wedge i \ge n$ gives $i = n$ and so $s = n(n+1)/2$. The bare formula $s = i(i+1)/2$ fails step (3): invariants often need an extra bound conjunct.

4. 4.

   The rule $\dfrac{b(s) = \mathrm{tt} \quad \langle c, s\rangle \Downarrow s' \quad \langle \mathtt{while}\ b\ \mathtt{do}\ c, s'\rangle \Downarrow t}{\langle \mathtt{while}\ b\ \mathtt{do}\ c, s\rangle \Downarrow t}$ has the same loop in its conclusion and in a premise. Structural induction on commands gives no hypothesis about that premise; induction on derivations does, because the sub-derivation is smaller. In Lean this is while_sound: generalize the command, then induction on the execution.

5. 5.

   $\mathsf{AG}\,\mathsf{EF}\,\mathit{init}$. The outer $\mathsf{AG}$ quantifies over every state reachable along any path; the inner $\mathsf{EF}$ asks for some path from that state to $\mathit{init}$. This property is not expressible in LTL, which cannot say "there exists a path".

6. 6.

   $Z_1 = \{3\}$, $Z_2 = \{2, 3\}$ (and $3$, by its self-loop), $Z_3 = \{1, 2, 3\}$, $Z_4 = \{1, 2, 3, 6\}$, $Z_5 = Z_4$. So $\mathsf{EF}\,p = \{1, 2, 3, 6\}$, which has $4$ states. States $4$ and $5$ form a cycle that never reaches $3$, so $\mathsf{AG}\,\neg p$ holds there.

7. 7.

   (a) and (b). Halting on a fixed input is the halting problem; totality is a non-trivial semantic property, so Rice's theorem applies. (c) is syntactic, (d) is model checking of a finite structure, and (e) is bounded — all decidable. This is why practical verification restricts programs, properties or automation.

8. 8.

   Option (a). With (a), loopForever_hoare proves {True} while true do skip {False}, since there are no runs at all. Option (b) would be false for that loop, which is the difference between partial and total correctness.

9. 9.

   (a), (b) and (c). The proof establishes a precise statement about formal models; anything that connects those models to reality — the source semantics, unverified tools, the hardware, and the proof checker itself — is assumed. Errors inside the checked proof (d) are exactly what the kernel rules out.

10. 10.

    from collections import deque
    
    def find_violation(initial, successors, is_bad):
        parent = {initial: None}
        queue = deque([initial])
        while queue:
            s = queue.popleft()
            if is_bad(s):
                path = []
                while s is not None:
                    path.append(s)
                    s = parent[s]
                return path[::-1]
            for t in successors(s):
                if t not in parent:
                    parent[t] = s
                    queue.append(t)
        return None
    

    Breadth-first search visits states in order of distance from the initial state, so the first bad state popped has a shortest path, and the parent map reconstructs it. Each state is enqueued once, so the search terminates on every finite system. Returning None is an exhaustive guarantee about the model — the same evidence as the lesson's model-checking experiment.