Incorrectness Logic for Graph Programs

Abstract

Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this ‘incorrectness logic’ to be sound and complete, and speculate on some possible future applications of it.

Appendix

Proof

(Proposition 1; Lemmata 1–2). By induction over the form of E-conditions, following the proof structure for transformations ‘App’, ‘A’, and ‘L’ for the similar assertion language in [24].    $\square$

Proof

(Proposition 2). $\Longrightarrow$. Assume that $H\models \mathrm {WPost}(\mathcal {R},c)$. There exists some $r\in \mathcal {R}$ such that:

$$\begin{aligned} H \models \mathrm {wpost}(r,c) = \exists \mathtt {x}_1,\cdots \mathtt {x}_n.\exists \emptyset \hookrightarrow R.\mathrm {Dang}(r^{-1})\wedge \mathrm {Right}(r, \mathrm {Shift}(r, c) ). \end{aligned}$$

There exists an $h\!: R^I\hookrightarrow G$ such that $h \models ^I \mathrm {Dang}(r^{-1})\wedge \mathrm {Right}(r, \mathrm {Shift}(r, c) )$. Using Proposition 1, there exists a direct derivation from some graph G to H via $r = \langle L\Rightarrow R \rangle$, and by Lemma 2, there exists some $g\!:L^I\hookrightarrow G$ such that $g \models ^I \mathrm {Shift}(r,c)$. By Lemma 1, $G\models c$.

$\Longleftarrow$. Assume that there exists a graph G such that $G\models c$ and $G\Rightarrow _\mathcal {R} H$. There exists some $r = \langle L \Rightarrow R \rangle \in \mathcal {R}$ such that $G\Rightarrow _r H$. By the definition of $\models$, Lemma 1, and Lemma 2, there exists some $h\!:R^I\hookrightarrow G \models ^I \mathrm {Right}(r,\mathrm {Shift}(r,c))$. By the definition of direct derivations and Proposition 1, $h \models ^I \mathrm {Dang}(r^{-1})$, and thus $h \models ^I \mathrm {Dang}(r^{-1}) \wedge \mathrm {Right}(r,\mathrm {Shift}(r,c))$. By the definition of $\models$, $H \models \exists \mathtt {x}_1,\cdots \mathtt {x}_n.\exists R.\mathrm {Dang}(r^{-1}) \wedge \mathrm {Right}(r,\mathrm {Shift}(r,c))$, that is, $H \models \mathrm {wpost}(r,c)$. Being a disjunct of $\mathrm {WPost}(r,c)$, we derive the result $H \models \mathrm {WPost}(r,c)$.    $\square$

Proof

(Theorem 1). Given $\vdash [c] P [\epsilon : d]$, we need to show that $\models [c] P [\epsilon : d]$. We consider each axiom and proof rule in turn and proceed by induction on proofs.

RuleSetSucc, RuleSetFail. The validity of these axioms follows immediately from the definitions of $\llbracket \mathcal {R} \rrbracket ok$, $\llbracket \mathcal {R} \rrbracket er$, Proposition 1, and Proposition 2.

SeqSucc. Suppose that $\vdash [c] P;Q [ok: d]$. By induction, we have $\models [c] P [ok: e]$ and $\models [e] Q [ok: d]$. By definition of $\models$, for all $H. H \models d$, there exists a $G'.G'\models e$ with $(G',G) \in \llbracket Q \rrbracket ok$, and for all $G'. G' \models e$, there exists a $G.G \models c$ with $(G,G') \in \llbracket P \rrbracket ok$. From the definition of $\models$ and $\llbracket P;Q \rrbracket ok$, it then follows that $\models [c] P;Q [ok: d]$. Analogous for case $\vdash [c] P;Q [er: d]$.

SeqFail. Suppose that $\vdash [c] P;Q [er: d]$. By induction, we have $\models [c] P [er: d]$. By definition of $\models$, for all $H. H \models d$, there exists a $G. G \models c$ with $(G,H) \in \llbracket P \rrbracket er$. By the definition of $\llbracket P;Q \rrbracket er$ and $\models$, it follows that $\models [c] P;Q [er: d]$.

IfElse. Suppose that $\vdash [c] \mathtt {if}\ \mathcal {R}\ \mathtt {then}\ P\ \mathtt {else}\ Q [\epsilon : d]$. By induction, $\models [c \wedge \mathrm {App}(\mathcal {R})] P [\epsilon : d]$ and $\models [c \wedge \lnot \mathrm {App}(\mathcal {R})] Q [\epsilon : d]$. From the definition of $\models$, $\llbracket \mathtt {if}\ \mathcal {R}\ \mathtt {then}\ P\ \mathtt {else}\ Q \rrbracket \epsilon$, and Proposition 1, we obtain the result that $\models [c] \mathtt {if}\ \mathcal {R}\ \mathtt {then}\ P\ \mathtt {else}\ Q [\epsilon : d]$.

Cons. Suppose that $\vdash [c] P [\epsilon : d]$. By induction, we have $\models [c'] P [\epsilon : d']$, $\models d \Longrightarrow d'$, and $\models c' \Longrightarrow c$. It immediately follows that $\models [c] P [\epsilon : d]$.

IterZero. For every graph $G. G\models c \wedge \lnot \mathrm {App}(\mathcal {R})$, by Proposition 1, $G\not \Rightarrow _\mathcal {R}$, $(G,G)\in \llbracket \mathcal {R}\rrbracket er$, and thus $(G,G) \in \llbracket \mathcal {R}! \rrbracket ok$. It immediately follows that $\models [c \wedge \lnot \mathrm {App}(\mathcal {R})] \mathcal {R}! [ok: c \wedge \lnot \mathrm {App}(\mathcal {R})]$.

Iter. Suppose that $\vdash [c \wedge \mathrm {App}(\mathcal {R})] \mathcal {R!} [ok: d \wedge \lnot \mathrm {App}(\mathcal {R})]$. By induction, $\models [c \wedge \mathrm {App}(\mathcal {R})] \mathcal {R;R!} [ok: d \wedge \lnot \mathrm {App}(\mathcal {R})$. By definition of $\models$, for all $H. H \models d \wedge \lnot \mathrm {App}(\mathcal {R})$, there exists some $G. G\models c \wedge \mathrm {App}(\mathcal {R})$ and $(G,H) \in \llbracket \mathcal {R};\mathcal {R}! \rrbracket ok$. By the definition of $\llbracket \mathcal {R}! \rrbracket ok$ and $\models$, we obtain $\models [c \wedge \mathrm {App}(\mathcal {R})] \mathcal {R!} [ok: d \wedge \lnot \mathrm {App}(\mathcal {R})]$.

IterVar. Suppose that $\vdash [c_0] \mathcal {R}! [ok: c_n]$. By induction, $\models [c_{i-1}] \mathcal {R} [ok: c_i]$ for every $0 < i \le n$ and $\models c_n \Longrightarrow \lnot \mathrm {App}(\mathcal {R})$. By the definition of $\models$ and $\llbracket \mathcal {R} \rrbracket ok$, for every $G_i. G_i \models c_i$, there exists some $G_{i-1}. G_{i-1} \models c_{i-1}$ and $G_{i-1} \Rightarrow _\mathcal {R} G_i$. It follow that there is a sequence of derivations $G_0 \Rightarrow _\mathcal {R} \cdots \Rightarrow _\mathcal {R} G_n$ with $G_0 \models c_0$ and $G_n \models c_n$. By $\models c_n \Longrightarrow \lnot \mathrm {App}(\mathcal {R})$ and Proposition 1, we have $G_n \not \Rightarrow _\mathcal {R}$, i.e. $(G_n,G_n) \in \llbracket \mathcal {R} \rrbracket er$. Together with the definition of $\llbracket \mathcal {R}! \rrbracket ok$, it follows that $\models [c_0] \mathcal {R}! [ok: c_n]$.    $\square$

Proof

(Theorem 2). We prove relative completeness extensionally by showing that for every program P, extensional assertion c, and exit condition $\epsilon \in \{ok, er\}$, $\vdash [c]P[\epsilon : \mathrm {WPOST}[P,c]]$, where $\mathrm {WPOST}[P,c]$ is an extensional assertion expressing the weakest postcondition relative to P and c, i.e. if $\models [c] P [\epsilon : d]$ for any d, then $d\Longrightarrow \mathrm {WPOST}[P,c]$ is valid. Relative completeness is obtained by applying the rule of consequence to $\vdash [c]P[\epsilon : \mathrm {WPOST}[P,c]]$.

Rule Application ($\epsilon = ok$). Immediate from RuleSetSucc and Cons.

Rule Application ($\epsilon = er$). Immediate from RuleSetFail, the definition of $\llbracket \mathcal {R} \rrbracket er$, and Cons.

Sequential Application ($\epsilon =ok$). In this case,

$$\begin{aligned}&\quad \quad \!\!\!H \models \mathrm {WPOST}[P;Q,c] \\&\mathrm {iff}\ \exists G. G\models c\ \text {and}\ (G,H) \in \llbracket P;Q \rrbracket ok\\&\mathrm {iff}\ \exists G,G'. G\models c, (G,G')\in \llbracket P \rrbracket ok,\ \text {and}\ (G',H)\in \llbracket Q \rrbracket ok\\&\mathrm {iff}\ \exists G'. G'\models \mathrm {WPOST}[P,c]\ \text {and}\ (G',H)\in \llbracket Q \rrbracket ok\\&\mathrm {iff}\ H \models \mathrm {WPOST}[Q,\mathrm {WPOST}[P,c]] \end{aligned}$$

By induction we have $\vdash [\mathrm {WPOST}[P,c]] Q [ok: \mathrm {WPOST}[Q,\mathrm {WPOST}[P,c]]]$ and $\vdash [c] P [ok: \mathrm {WPOST}[P,c]]$. By SeqSucc we derive the triple $\vdash [c] P;Q [ok: \mathrm {WPOST}[Q,\mathrm {WPOST}[P,c]]]$, and by Cons $\vdash [c] P;Q [ok: \mathrm {WPOST}[P;Q,c]]$.

Sequential Application ($\epsilon =er$). If the program P; Q fails and the error occurs in Q, then the proof is analogous to the ok case. If the error occurs in P:

$$\begin{aligned}&\quad \quad H \models \mathrm {WPOST}[P;Q,c]\\&\mathrm {iff}\ \exists G. G\models c\ \text {and}\ (G,H) \in \llbracket P;Q \rrbracket er\\&\mathrm {iff}\ \exists G. G\models c\ \text {and}\ (G,H) \in \llbracket P \rrbracket er\\&\mathrm {iff}\ H \models \mathrm {WPOST}[P,c] \end{aligned}$$

By induction we have $\vdash [c] P [ er: \mathrm {WPOST}[P,c]]$, and by SeqFail derive $\vdash [c] P;Q [er: \mathrm {WPOST}[P,c]]$. With Cons we get $\vdash [c] P;Q [er: \mathrm {WPOST}[P;Q,c]]$.

If-then-else. The proof for this case follows a similar structure to sequential composition but treating the two branches separately.

Iteration. Define $c_i$ as $\mathrm {WPOST}[\mathcal {R},c_{i-1}]$ for every $0 < i \le n$. We have:

$$\begin{aligned}&\quad \quad G_n \models \mathrm {WPOST}[\mathcal {R!},c_0]\\&\mathrm {iff}\ \exists G_0. G_0 \models c_0\ \text {and}\ (G_0,G_n) \in \llbracket \mathcal {R!} \rrbracket ok\\&\mathrm {iff}\ \exists G_0,\cdots G_{n-1}. (G_{i-1},G_i) \in \llbracket \mathcal {R} \rrbracket ok\ \text {for all}\ 0< i \le n,\ \text {and}\ (G_n, G_n) \in \llbracket \mathcal {R} \rrbracket er \\&\mathrm {iff}\ \exists G_1,\cdots G_{n-1}. G_1 \models \mathrm {WPOST}[\mathcal {R},c_0],\ (G_{i-1},G_i) \in \llbracket \mathcal {R} \rrbracket ok\ \text {for all}\ 1 < i \le n\\&\ \ \text {and}\ (G_n, G_n) \in \llbracket \mathcal {R} \rrbracket er \\&\mathrm {iff}\ G_n \models c_n\ \text {and}\ c_n \Longrightarrow \lnot \mathrm {App}(\mathcal {R}) \end{aligned}$$

By induction, $\vdash [c_{i-1}] \mathcal {R} [ok: \mathrm {WPOST}[\mathcal {R},c_{i-1}]]$ and thus $\vdash [c_{i-1}] \mathcal {R} [ok: c_i]$. By IterVar and Cons derive the result, $\vdash [c_0] \mathcal {R!} [ok: \mathrm {WPOST}[\mathcal {R!},c_0]]$.    $\square$