${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t_{0}^{*}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}}\alpha(p)=\alpha(q)$ so that
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{0}^{*}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}$
and the completeness of the  ok part yields
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{0}^{*}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}$.
By Lemma 5
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{0}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(q)=\alpha(s)$, meaning that
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[q]\;\mathtt{t_{0}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$
and by induction
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[q]\;\mathtt{t_{0}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$.
By (rec-err) we obtain
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{0}^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$.

In order to use (relax), we need to ensure that the additional conditions
$r\leq s$ and $\alpha(r)=\alpha(s)$ are satisfied. By
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{0}^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
and (32),
$r\leq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{0}^{*}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p=s$ and
$\alpha(r)=\alpha({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{0}^{*}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p)=\alpha({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{0}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t_{0}^{*}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}p)=\alpha(s)$, so that (relax) yields the result
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{0}^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.
∎

###### Example 4.4

Consider a relational bdKAT $K\triangleq\wp({\mathbb{Z}}\times{\mathbb{Z}})$
on the set of integers ${\mathbb{Z}}$, where
$\textbf{1}_{K}\triangleq\\{\langle{z,z}\rangle\mid z\in{\mathbb{Z}}\\}$ and
$\textbf{0}_{K}\triangleq\varnothing$, and the standard integer interval
abstraction $\operatorname{Int}$ [9, 10]. Let us consider a language with
primitive actions
$\Sigma\triangleq\\{\mathtt{x:=x+1},\operatorname{\mathtt{err}}\\}$. The
evaluation function $u:\Sigma\cup B\rightarrow
K_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}\times
K_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}$ is defined as expected:

$\displaystyle u(\mathtt{x:=x+1})$
$\displaystyle=(\\{\langle{z,z+1}\rangle\mid
z\in\mathbb{Z}\\},\textbf{0}_{K}),$ $\displaystyle
u(\operatorname{\mathtt{err}})=(\textbf{0}_{K},\textbf{1}_{K}).$

We study the correctness of the program
${\mathtt{r}\equiv((\mathtt{x:=x+1})+\operatorname{\mathtt{err}})^{*}}$, for
the precondition $p\triangleq\\{\langle{0,0}\rangle,\langle{2,2}\rangle\\}$
and the specification
$\operatorname{Spec}\triangleq(\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}\\!:\\{\langle{z,z}\rangle\mid z\geq
0\\},\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}\\!:\textbf{0}_{K})$. Let us define an auxiliary sequence of tests
$p_{n}\triangleq\\{\langle{n,n}\rangle,\langle{n+2,n+2}\rangle\\}$ and
$s\triangleq\\{\langle{z,z}\rangle\mid z\geq 0\\}$.

We can easily check the local completeness of the atoms by exploiting the
characterization of the backward diamond operator in relational KATs of Lemma
2.

We therefore have the following derivation in
$\operatorname{LCIL}_{\operatorname{Int}}$ for $\mathtt{r}$:

$\mathbb{C}^{\operatorname{Int}}_{p_{n}}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{x:=x+1}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}})$
$\mathbb{C}^{\operatorname{Int}}_{p_{n}}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{x:=x+1}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[p_{n}]\;\mathtt{x:=x+1}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:p_{n+1}]}$
$\mathbb{C}^{\operatorname{Int}}_{p_{n}}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{\operatorname{\mathtt{err}}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}})$
$\mathbb{C}^{\operatorname{Int}}_{p_{n}}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{\operatorname{\mathtt{err}}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[p_{n}]\;\mathtt{\operatorname{\mathtt{err}}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:0]}$
(choice)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[p_{n}]\;\mathtt{(\mathtt{x:=x+1})+\operatorname{\mathtt{err}}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:p_{n+1}]}$
(limit) $\dagger$

$\mathbb{C}^{\operatorname{Int}}_{s}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{x:=x+1}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}})$
$\mathbb{C}^{\operatorname{Int}}_{s}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{x:=x+1}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[s]\;\mathtt{x:=x+1}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:0]}$
$\mathbb{C}^{\operatorname{Int}}_{s}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{\operatorname{\mathtt{err}}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}})$
$\mathbb{C}^{\operatorname{Int}}_{s}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{\operatorname{\mathtt{err}}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[s]\;\mathtt{\operatorname{\mathtt{err}}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$
(choice) $\ddagger$

$\dagger$ (limit)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[p_{0}]\;\mathtt{((\mathtt{x:=x+1})+\operatorname{\mathtt{err}})^{*}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:s]}$
$\ddagger$ (choice)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[s]\;\mathtt{(\mathtt{x:=x+1})+\operatorname{\mathtt{err}}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$
(rec-err)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{\operatorname{Int}}[p_{0}]\;\mathtt{((\mathtt{x:=x+1})+\operatorname{\mathtt{err}})^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$

By soundness of $\operatorname{LCIL}_{\operatorname{Int}}$ in Theorem 4.2, the
program $\mathtt{r}$ satisfies the  ok part of $\operatorname{Spec}$ because

${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{r}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}p\subseteq\operatorname{Int}(s)=s\subseteq
s=\operatorname{Spec}_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}.$

However, the  err part is not satisfied as
$\operatorname{Int}(s)=s\nsubseteq\varnothing=\textbf{0}_{K}=\operatorname{Spec}_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}$. Moreover, $\operatorname{LCIL}_{\operatorname{Int}}$ also catches
true alerts as
$s\smallsetminus\operatorname{Spec}_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}=s$. ∎

###  4.1 Relationship with Incorrectness logic

$\mathtt{a}\in\operatorname{Atom}$ (transfer)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{a}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{a}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}p]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{a}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p]}$

$\mathtt{a}\in\operatorname{Atom}$ (empty)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:0]}$

$p^{\prime}\leq
p\qquad\vdash_{\operatorname{IL}}[p^{\prime}]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q^{\prime}]}\qquad
q\leq q^{\prime}$ (consequence)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$

$\vdash_{\operatorname{IL}}[p_{1}]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q_{1}]}$
$\vdash_{\operatorname{IL}}[p_{2}]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q_{2}]}$
(disj)
$\vdash_{\operatorname{IL}}[p_{1}+p_{2}]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q_{1}+q_{2}]}$

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{\text{$1$}}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:q]}$
(short-circuit) $\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:q]}$

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{\text{$1$}}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:r]}\\!\\!$
$\\!\\!\vdash_{\operatorname{IL}}[r]\;\mathtt{t_{\text{$2$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$
(seq-normal) $\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{1}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:r]}$
(iterate zero)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t^{*}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:p]}$

$\forall
n\in\mathbb{N}.\;\vdash_{\operatorname{IL}}[p_{n}]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:p_{n+1}]}$
(back-v)
$\vdash_{\operatorname{IL}}[p_{0}]\;\mathtt{t^{*}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:\bigvee_{n\in\mathbb{N}}p_{n}]}$

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t^{*}\cdot
t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$
(iterate non-zero)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t^{*}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{\text{$i$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$,
with $i\in\\{1,2\\}$ (choice)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$

Figure 4: Proof system $\operatorname{IL}$.

Section 3.6 has shown that $\operatorname{LCK}$ yields a generalization of
$\operatorname{UL}$. The same can be done for $\operatorname{IL}$, i.e., we
prove that $\operatorname{LCIL}_{A}$ with incorrectness triples generalizes
the incorrectness logic of [26]. For the sake of clarity, we recall in Figure
4 an algebraic version of $\operatorname{IL}$. Analogously to the reduction of
Theorem 3.6, this generalization is obtained by letting $A=A_{tr}$, where
$A_{tr}$ is the trivial abstract domain.

######  Theorem 4.5 ()

Let $K$ be a CTC bdKAT and $T_{\Sigma,B}$ a language interpreted on $K$. For
any $p,q\in\operatorname{\mathsf{test}}(K)$, $\mathtt{t}\in T_{\Sigma,B}$,

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}\quad\Leftrightarrow\quad\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}.$

###### Proof

Notice that the  ok part of $\operatorname{LCIL}$ coincides with
$\operatorname{LCK}$222With the additional rule (limit) and without the rules
(rec), (iterate). and likewise $\operatorname{IL}$ coincides with
$\operatorname{UL}$. Hence this part of the equivalence follows by Theorem
3.6. We only need to show the equivalence of the  err part.

$\Rightarrow)$ Assuming
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
we need to show
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.
The proof is by induction on the derivation tree.

(tranfer) : Coincides with (transfer).
(relax) : Coincides with (consequence).
(seq-ok) : Is the  ok part of (seq-normal).
(seq-err) : Can be derived as follows

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{1}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}$
$\vdash_{\operatorname{IL}}[q]\;\mathtt{t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$
(seq-normal) $\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{1}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
(short-circuit) $\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
(disj) $\vdash_{\operatorname{IL}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s+r]}$

(rec-err) : Can be derived as follows

$\vdash_{\operatorname{IL}}[p]\;\mathtt{t^{*}}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}$
$\vdash_{\operatorname{IL}}[q]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
(seq-normal) $\vdash_{\operatorname{IL}}[p]\;\mathtt{t^{*}\cdot
t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
(iterate non-zero)
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$

(join) : As in Theorem 3.6.
(limit) : Coincides with (back-v).

$\Leftarrow)$ Assuming
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
we need to show
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.
As in Theorem 3.6, we exploit the completeness of $\operatorname{LCIL}$ and
likewise we observe that the condition (2) is trivially true as
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}\alpha(p)=\top=\alpha(q)=\top=\alpha({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p)$, meaning that the only condition to check is (1). The proof is by
structural induction on the derivation tree of
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.

(transfer) : The premises
$\mathbb{C}^{A}_{p}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{a}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$ and
$\mathbb{C}^{A}_{p}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{a}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}})$ hold for any $\mathtt{a}$ and $p$ because $A_{tr}(\cdot)=1$, so that
(transfer) yields
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{a}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{a}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p]}$.

(empty) : For any $\mathtt{t}\in T_{\Sigma,B}$ it holds
$0\leq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p$, meaning
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:0]}$
and by completeness of $\operatorname{LCIL}$ we have
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:0]}$.

(consequence) : The inequalities $p\leq A_{tr}(p^{\prime})$ and
$q^{\prime}\leq A_{tr}(q)$ are always true because $A_{tr}(\cdot)=1$ which is
the greatest element of $\operatorname{\mathsf{test}}(K)$ meaning that the
rule coincides with (relax).

(disj) and (choice) : Same as in Theorem 3.6.

(short-circuit) : By induction
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
and by soundness
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.
By (31)
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}p\geq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p\geq r$ which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
and by completeness
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.

(seq-normal) : By induction and soundness we have
$r\leq{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}p$ and
$q\leq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}r$. By (31)
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}p\geq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t_{1}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}p\geq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}r\geq q$, which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:q]}$
and by completeness
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:q]}$.

(iterate non-zero) : By induction and soundness

$q\leq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t^{*}\cdot
t}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p\stackrel{{\scriptstyle(\ref{eqn:csema_err_mul})}}{{=}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t^{*}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}p+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t^{*}}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}p\stackrel{{\scriptstyle(\ref{eqn:csema_err_star})}}{{=}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t^{*}}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p$

which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:q]}$
and by completeness
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:q]}$.
∎

The abstraction map $\alpha=\lambda x.\top$ of $A_{tr}$ makes the validity of
a triple trivially true. In particular,
${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{{A_{tr}}_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}}\alpha(p)=\top=\alpha(q)=\alpha({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}p)$ and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{{A_{tr}}_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}\alpha(p)=\top=\alpha(q)=\alpha({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}p)$ hold. As a consequence, we obtain that

$\displaystyle\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}\quad\Leftrightarrow\quad\>\models_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
(34)

By this equivalence (34) and Theorems 4.2 and 4.3, we can thus retrieve the
logical soundness and completeness of $\operatorname{IL}$ as a consequence of
the one of $\operatorname{LCIL}_{A_{tr}}$.

###### Corollary 2

Let $K$ be a CTC bdKAT and $T_{\Sigma,B}$ a language interpreted on $K$. For
any $p,q\in\operatorname{\mathsf{test}}(K)$, $\mathtt{t}\in T_{\Sigma,B}$,
$\vdash_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}\;\Leftrightarrow\;\>\models_{\operatorname{IL}}[p]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.

##  5 Local Completeness Logic in TopKAT

We have shown in Section 3 how KAT extended with a modal backward-diamond
operator allows us to interpret and represent the local completeness program
logic. This result follows the approach by Moller, O’Hearn and Hoare [24], who
leverage a backward-diamond operator in their KAT interpretation of
correctness/incorrectness logics. On the other hand, Zhang, de Amorim and
Gaboardi [34] have recently shown that incorrectness logic can be formulated
for a standard KAT, provided that it contains a top element, thus giving rise
to a so-called TopKAT. In particular, [34] observed that a TopKAT is enough to
express the codomain of relational KATs. In this section, we take a similar
path in studying an alternative formulation of local completeness logic based
on a TopKAT.

###  5.1 Abstracting TopKATs

We expect that the base case of abstract semantics
$\llbracket\mathtt{\mathtt{a}}\rrbracket_{A}^{\sharp}p^{\sharp}$ for a basic
action $\mathtt{a}\in\operatorname{Atom}$ is defined as best correct
approximation in $A$ of the concrete semantics of $\mathtt{a}$ on the
concretization of $p^{\sharp}$. In a bdKAT this is achieved in definition
(LABEL:def:abs-sem) through its backward-diamond operator, which is crucially
used in (11) to define the strongest postcondition as
$\llbracket\mathtt{a}\rrbracket^{K}\gamma(p^{\sharp})=\boldsymbol{\langle}\llbracket\mathtt{a}\rrbracket_{u}\boldsymbol{|}\gamma(p^{\sharp})$.
Zhang et al. [34] observed that in a relational model of KAT, the codomain
inclusion $\operatorname{cod}(q)\subseteq\operatorname{cod}(pa)$ defining the
meaning of an under-approximation triple $[p]\,a\,[q]$ can be expressed in a
TopKAT as the inequality $\top q\leq\top pa$, thus hinting that this latter
condition could be taken as definition of validity of incorrectness triples in
a TopKAT. We follow here a similar approach by considering the element $\top
p\llbracket\mathtt{a}\rrbracket_{u}$ as a proxy for strongest postconditions
in a TopKAT. It is worth noticing that while in a bdKAT a strongest
postcondition
$\boldsymbol{\langle}\llbracket\mathtt{a}\rrbracket_{u}\boldsymbol{|}p$ is
always a test, in a TopKAT $K$, given $p\in\operatorname{\mathsf{test}}(K)$
and a term $\mathtt{t}\in T_{\Sigma,B}$, it is not guaranteed that there
exists a test $q\in\operatorname{\mathsf{test}}(K)$ such that $\top
p\llbracket\mathtt{t}\rrbracket_{u}=\top q$, as shown by the following
example.

######  Example 5.1 (Strongest Postconditions in TopKAT)

Consider the Kleene algebra $A_{3}=\\{0,1,a\\}$ consisting of 3 elements and
characterized by Conway [8, Chapter 12]. This algebra can be lifted to a KAT
by letting $\operatorname{\mathsf{test}}(A_{3})\triangleq\\{0,1\\}$ and
defining the KAT operators as follows:

$\begin{array}[]{|c|ccc|}\hline\cr~{}+{}&~{}0{}&~{}1{}&~{}a{}\\\ \hline\cr
0&0&1&a\\\ 1&1&1&1\\\ a&a&1&a\\\ \hline\cr\end{array}$
$\begin{array}[]{|c|ccc|}\hline\cr~{}\cdot{}&~{}0{}&~{}1{}&~{}a{}\\\ \hline\cr
0&0&0&0\\\ 1&0&1&a\\\ a&0&a&0\\\ \hline\cr\end{array}$
$\begin{array}[]{|c|c|c|}\hline\cr\rule{0.0pt}{12.0pt}~{}\mathord{0^{*}}\triangleq
1{}&~{}\mathord{1^{*}}\triangleq 1&~{}\mathord{a^{*}}\triangleq
1~{}\rule{0.0pt}{12.0pt}\\\ \hline\cr\end{array}$

We have that $1\geq a$ and $1\geq 0$, because $1+a=1$ and $1+0=1$, so that
$A_{3}$ is a TopKAT with $\top=1$. Moreover, $\top\cdot 1\cdot a=1\cdot 1\cdot
a=a$, whereas there exists no $q\in\operatorname{\mathsf{test}}(A_{3})$
satisfying $\top\cdot q=a$. Indeed, $\top\cdot 1=1\cdot 1=1\neq a$ and
$\top\cdot 0=0\neq a$. ∎

In general, the lack of such a $q\in\operatorname{\mathsf{test}}(K)$ implies
that the abstract domain cannot be defined as an abstraction of the set of
topped-tests $\\{\top p\mid p\in\operatorname{\mathsf{test}}(K)\\}$, because
in this case we could miss the abstraction $\alpha(\top
p\llbracket\mathtt{a}\rrbracket_{u})$. To settle this issue, an abstract
domain must provide an approximation of the larger set

$\operatorname{\mathsf{top}}(K)\triangleq\\{\top a\mid a\in K\\}$

which contains all the multiplicative elements of type $\top a$.

######  Definition 5.2 (Top Kleene Abstract Domain)

A poset $(A,\leq)$ is a _top Kleene abstract domain_ of a TopKAT $K$ if:

  1. (i)

There exists a Galois insertion, defined by
$\gamma:A\rightarrow\operatorname{\mathsf{top}}(K)$ and
$\alpha:\operatorname{\mathsf{top}}(K)\rightarrow A$, of the poset
$(A,\leq_{A})$ into the poset $(\operatorname{\mathsf{top}}(K),\leq_{K})$;

  2. (ii)

$A$ is countably-complete. ∎

The abstract semantic function
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}:T_{\Sigma,B}\rightarrow(A\rightarrow
A)$ on a top Kleene abstraction $A$ can be therefore defined for the base case
$\mathtt{a}\in\operatorname{Atom}$ as

$\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}p^{\sharp}\triangleq\alpha(\gamma(p^{\sharp})\llbracket\mathtt{a}\rrbracket_{u}),$

while the remaining inductive cases are defined as in (LABEL:def:abs-sem) for
Kleene abstractions. The monotonicity and soundness properties of this
abstract semantics hold, provided that the TopKAT is ∗-continuous333This
condition plays a role similar to the CTC condition for bdKATs., which is
referred to as TopKAT∗.

######  Theorem 5.3 (Soundness of TopKAT Abstract Semantics)

Let $A$ be a Kleene abstraction of a TopKAT∗ $K$ and $T_{\Sigma,B}$ be a
language interpreted on $K$. For all $p^{\sharp},q^{\sharp}\in A$, $a\in K$
and $\mathtt{t}\in T_{\Sigma,B}$:

$\displaystyle
p^{\sharp}\leq_{A}q^{\sharp}\Rightarrow\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}p^{\sharp}\leq_{A}\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}q^{\sharp}$
(monotonicity) $\displaystyle\alpha(\top
a\llbracket\mathtt{t}\rrbracket_{u})\leq_{A}\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top
a)$ (soundness)

###### Proof

The first property can be proved by induction on the structure of
$\mathtt{t}\in T_{\Sigma,B}$. Notice that the inductive cases are the same as
Theorem 3.2, therefore we only need to verify the base case.

$\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}p^{\sharp}=\alpha(\gamma(p^{\sharp})\llbracket\mathtt{a}\rrbracket_{u})\leq\alpha(\gamma(q^{\sharp})\llbracket\mathtt{a}\rrbracket_{u})=\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}q^{\sharp}$

where we used the isotony of $\alpha(\cdot)$, $\gamma(\cdot)$ and $\cdot$.

Likewise we prove the second property by induction on the structure of
${\mathtt{t}\in T_{\Sigma,B}}$. The computation can be easily adapted from
Theorem 3.2. As an example we explicitly prove the $\mathtt{t_{0}^{*}}$ case.

($\mathtt{t_{0}^{*}}$) : In order to prove the result we need a preliminary
fact

$\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)$ (35)

which can be shown by induction on $n$. The base case holds as $\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{0})=\alpha(\top
a)=(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{0}\alpha(\top a)$. The
inductive case can be proved as follows

$\alpha(\top a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n+1})=\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}\llbracket\mathtt{t_{0}}\rrbracket_{u})\leq\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n+1}\alpha(\top
a)$

The previous fact and the ∗-continuity of $K$ yield the soundness

$\displaystyle\alpha(\top a\llbracket\mathtt{t_{0}^{*}}\rrbracket_{u})$
$\displaystyle=$ $\displaystyle\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{*})$ $\displaystyle=\textrm{[By
${}^{*}$-continuity]}$ $\displaystyle\alpha(\bigvee_{n\in\mathbb{N}}\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})$ $\displaystyle=\textrm{[By
additivity of $\alpha(\cdot)$]}$
$\displaystyle\bigvee_{n\in\mathbb{N}}\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})$ $\displaystyle\leq\textrm{[By
(\ref{eqn:claim_4})]}$
$\displaystyle\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)$ $\displaystyle=$
$\displaystyle\llbracket\mathtt{t_{0}^{*}}\rrbracket_{A}^{\sharp}\alpha(\top
a).$ ∎

###  5.2 Local Completeness Logic on TopKAT

Completeness and triple validity are adapted to the TopKAT framework as
follows. Given a Top Kleene abstract domain $A$ on a TopKAT∗ $K$, $A$ is
defined to be locally complete for $a\in K$ on an element $b\in K$, denoted by
$\mathbb{C}^{A}_{b}(a)$, when

$A(\top ba)=A(A(\top b)a)$

holds. Moreover, $A$ is globally complete for $a$, denoted by
$\mathbb{C}^{A}(a)$, when it is locally complete for any $b\in K$.

Likewise, a triple $[a]\;\mathtt{t}\;[b]$, with $a,b\in K$ and $\mathtt{t}\in
T_{\Sigma,B}$, is valid, denoted by
${\models^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;[b]}$, when:

(1) $\top b\leq\top a\llbracket\mathtt{t}\rrbracket_{u}$; (2)
$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top a)=\alpha(\top
b)=\alpha(\top a\llbracket\mathtt{t}\rrbracket_{u})$.

The corresponding proof system, denoted by $\operatorname{LCTK}_{A}$, has the
same rules of $\operatorname{LCK}_{A}$ in Figure 1 except (transfer), (relax)
and (iterate) which are modified as follows:

$\mathtt{c}\in\operatorname{Atom}$
$\mathbb{C}^{A}_{a}(\llbracket\mathtt{c}\rrbracket_{u})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{c}\;[a\llbracket\mathtt{c}\rrbracket_{u}]$

$\top a^{\prime}\leq\top a\leq A(\top
a^{\prime})\qquad\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a^{\prime}]\;\mathtt{t}\;[b^{\prime}]\qquad\top
b\leq\top b^{\prime}\leq A(\top b)$ (relax)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;[b]$

$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;[b]$ $\top b\leq
A(\top a)$ (iterate)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t^{*}}\;[a+b]$

This incarnation $\operatorname{LCTK}_{A}$ of local completeness logic for
TopKAT∗ turns out to be logically sound and, under additional hypotheses,
complete.

######  Theorem 5.4 (Logical Soundness of
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}$)

If $\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;[b]$ then

  1. (i)

$\top b\leq\top a\llbracket\mathtt{t}\rrbracket_{u}$;

  2. (ii)

$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top a)=\alpha(\top
b)=\alpha(\top a\llbracket\mathtt{t}\rrbracket_{u})$.

###### Proof

The proof is as in Theorem 3.4. As an example we explicitly prove the cases
(transfer) and (iterate).

(transfer) : (i) is immediate because $\top b=\top
a\llbracket\mathtt{c}\rrbracket_{u}\leq\top
a\llbracket\mathtt{c}\rrbracket_{u}$. (ii) instead is a consequence of local
completeness ${\llbracket\mathtt{c}\rrbracket_{A}^{\sharp}\alpha(\top
a)=\alpha(\gamma(\alpha(\top
a))\llbracket\mathtt{c}\rrbracket_{u})\stackrel{{\scriptstyle\text{LC}}}{{=}}\alpha(\top
a\llbracket\mathtt{c}\rrbracket_{u})=\alpha(\top b)}$.

(iterate) : For any $k\in K$ it holds $1\leq k^{*}$ and $k\leq k^{*}$ [18,
Section 2.1]. In particular $\top b\leq\top
a\llbracket\mathtt{t}\rrbracket_{u}\leq\top
a(\llbracket\mathtt{t}\rrbracket_{u})^{*}$ and $\top a=\top a\cdot 1\leq\top
a(\llbracket\mathtt{t}\rrbracket_{u})^{*}$, thus implying (i)
${\top(a+b)\leq\top a(\llbracket\mathtt{t}\rrbracket_{u})^{*}=\top
a\llbracket\mathtt{t^{*}}\rrbracket_{u}}$. To show the (ii) we need a
preliminary fact

$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top a)\leq\alpha(\top
a)\Rightarrow\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)=\alpha(\top a)$ (36)

As a first step, let us prove by induction on $n$ that $\alpha(\top a)$ is an
upper-bound of the elements of the disjunction, i.e., $\forall
n\in\mathbb{N}.\;(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)\leq\alpha(\top a)$. The base case is trivially true
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{0}\alpha(\top a)=\alpha(\top
a)\leq\alpha(\top a)$, while the inductive case can be shown as follows:
${(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n+1}\alpha(\top
a)=(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top
a)\leq(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)\leq\alpha(\top a)}$. Notice that $\alpha(\top a)$ is also the least upper
bound because it is part of the disjunction as
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{0}\alpha(\top a)=\alpha(\top
a)$. The hypothesis $\top b\leq A(\top a)$ can be rewritten as $\alpha(\top
b)\leq\alpha(\top a)$ by isotony of $\alpha(\cdot)$,$\gamma(\cdot)$, (21),
(23). Finally, $\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top
a)=\alpha(\top b)\leq\alpha(\top a)$, meaning that the premise of (36) holds,
so that we can conclude

$\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(\top
a)=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)=\alpha(\top a)=\alpha(\top a)+\alpha(\top b)=\alpha(\top(a+b))$

∎

Logical completeness needs the following additional conditions:

  1. (a)

Likewise $\operatorname{LCK}_{A}$, the same infinitary rule for Kleene star:

$\forall
n\in\mathbb{N}.\;\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{n}]\;\mathtt{t}\;[a_{n+1}]$
(limit)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{0}]\;\mathtt{t^{*}}\;[\bigvee_{n\in\mathbb{N}}a_{n}]$

where we assume that:

     * •

$\bigvee_{n\in\mathbb{N}}a_{n}$ always exists. Let us remark that for bdKAT,
such explicit condition was not needed, as it was entailed by the CTC
requirement on the KAT.

     * •

$\top$ distributes over $\bigvee_{n\in\mathbb{N}}a_{n}$, i.e.,
$\top\bigvee_{n\in\mathbb{N}}a_{n}=\bigvee_{n\in\mathbb{N}}\top a_{n}$.

  2. (b)

Global completeness of all the primitive actions and tests occurring in the
program.

As in $\operatorname{LCK}_{A}$, (limit) is sound:

######  Lemma 6 ()

With the hypothesis of Theorem 5.4, the rule (limit) is logically sound.

###### Proof

Instantiating (i) we obtain $\top\bigvee_{n\in\mathbb{N}}a_{n}\leq\top
a_{0}\llbracket\mathtt{t^{*}}\rrbracket_{u}$. The distributivity condition of
(limit) yields $\top\bigvee_{n\in\mathbb{N}}a_{n}=\bigvee_{n\in\mathbb{N}}\top
a_{n}$. For this reason (i) is equivalent to ${\forall n\in\mathbb{N}.\;\top
a_{0}\llbracket\mathtt{t^{*}}\rrbracket_{u}\geq\top a_{n}}$. This fact can be
shown by induction on $n$.

For $n=0$ : $\top a_{0}\llbracket\mathtt{t^{*}}\rrbracket_{u}=\top
a_{0}(\llbracket\mathtt{t}\rrbracket_{u})^{*}\geq\top a_{0}$, as for any $k\in
K$, $k^{*}\geq 1$ by ($*$-unfold).

For $n+1$ : The rule has a premise
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{n}]\;\mathtt{t}\;[a_{n+1}]$,
and by induction (on the derivation tree) we have that
$\models^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{n}]\;\mathtt{t}\;[a_{n+1}]$.

$\displaystyle\top a_{0}\llbracket\mathtt{t^{*}}\rrbracket_{u}$
$\displaystyle=$ $\displaystyle\top
a_{0}(\llbracket\mathtt{t}\rrbracket_{u})^{*}$ $\displaystyle\geq\textrm{[By
(\ref{eqn:star_unfold})]}$ $\displaystyle\top
a_{0}(1+(\llbracket\mathtt{t}\rrbracket_{u})^{*}\llbracket\mathtt{t}\rrbracket_{u})$
$\displaystyle\geq$ $\displaystyle\top
a_{0}(\llbracket\mathtt{t}\rrbracket_{u})^{*}\llbracket\mathtt{t}\rrbracket_{u}$
$\displaystyle=$ $\displaystyle\top
a_{0}\llbracket\mathtt{t^{*}}\rrbracket_{u}\llbracket\mathtt{t}\rrbracket_{u}$
$\displaystyle\geq$ $\displaystyle\top
a_{n}\llbracket\mathtt{t}\rrbracket_{u}$ $\displaystyle\geq\textrm{[By
$\models^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{n}]\;\mathtt{t}\;[a_{n+1}]$]}$
$\displaystyle\top a_{n+1}$

For condition (ii) instead we need to show
$\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(\top
a_{0})=\alpha(\top\bigvee_{n\in\mathbb{N}}a_{n})$, provided that
$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top a_{n})=\alpha(\top
a_{n+1})$. By definition,
$\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(\top
a_{0})=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a_{0})$ and we have also that
$\alpha(\top\bigvee_{n\in\mathbb{N}}a_{n})=\alpha(\bigvee_{n\in\mathbb{N}}\top
a_{n})=\bigvee_{n\in\mathbb{N}}\alpha(\top a_{n})$. Therefore (ii) is implied
by

$\forall
n\in\mathbb{N}.\;(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a_{0})=\alpha(\top a_{n})$

That can be show by induction on $n$. The base case is trivial
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{0}\alpha(\top
a_{0})=\alpha(\top a_{0})$, while the inductive can be shown as follows

$\displaystyle(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n+1}\alpha(\top
a_{0})=\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a_{0})=\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top
a_{n})=\alpha(\top a_{n+1}).$ ∎

Condition (b) entails global completeness:

######  Lemma 7 ()

Let $K$ a TopKAT∗, $A$ a top Kleene abstract domain on $K$ and $T_{\Sigma,B}$
a KAT language on $K$. For any $\mathtt{t}\in T_{\Sigma,B}$ and $a\in K$ we
have

$(\forall\mathtt{b}\in\operatorname{Atom}(\mathtt{t}).\;\mathbb{C}^{A}(\llbracket\mathtt{b}\rrbracket_{u}))\Rightarrow\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(\top
a)=\alpha(\top a\llbracket\mathtt{t}\rrbracket_{u})$

###### Proof

The proof is as in Lemma 4. We only prove explicitly the $\mathtt{t_{0}^{*}}$
case.

$(\mathtt{t_{0}^{*}})$ : The result is a consequence of the following claim

$\forall
n\in\mathbb{N}.\;(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)=\alpha(\top a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})$ (37)

that can be proved by induction. The base case is as follows:
$(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{0}\alpha(\top
a)=\alpha(\top a)=\alpha(\top a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{0})$.
The inductive case can be proved as follows

$\displaystyle(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n+1}\alpha(\top
a)$ $\displaystyle=$
$\displaystyle\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)$ $\displaystyle=$
$\displaystyle\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})$ $\displaystyle=$
$\displaystyle\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}\llbracket\mathtt{t_{0}}\rrbracket_{u})$
$\displaystyle=$ $\displaystyle\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n+1})$

Moreover by ∗-continuity we have that $\top
a\llbracket\mathtt{t_{0}^{*}}\rrbracket_{u}=\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{*}=\bigvee_{n\in\mathbb{N}}\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}$, meaning that

$\displaystyle\llbracket\mathtt{t_{0}^{*}}\rrbracket_{A}^{\sharp}\alpha(\top
a)$ $\displaystyle=$
$\displaystyle\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(\top
a)$ $\displaystyle=\textrm{[By (\ref{eqn:claim_5})]}$
$\displaystyle\bigvee_{n\in\mathbb{N}}\alpha(\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})$
$\displaystyle=\textrm{[Additivity of $\alpha(\cdot)$)]}$
$\displaystyle\alpha(\bigvee_{n\in\mathbb{N}}\top
a(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n})$ $\displaystyle=$
$\displaystyle\alpha(\top a\llbracket\mathtt{t_{0}^{*}}\rrbracket_{u})$ ∎

######  Theorem 5.5 (Logical Completeness of
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}$)

Assume that conditions (a) and (b) hold. If
$\models^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;[b]$ then
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;[b]$.

###### Proof

The proof is as in Theorem 3.5. The case $(\mathtt{t_{0}^{*}})$ requires
special attention, and is proved explicitly.

($\mathtt{t_{0}^{*}}$) : Let
$a_{n}=a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}$. As a first step we
prove that ${\forall
n\in\mathbb{N}.\;\models^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{n}]\;\mathtt{t_{0}}\;[a_{n+1}]}$:
condition (i) holds because $\top a_{n+1}=\top
a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n+1}=\top
a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}\llbracket\mathtt{t_{0}}\rrbracket_{u}=\top
a_{n}\llbracket\mathtt{t_{0}}\rrbracket_{u}$, while (ii) holds by Lemma 7,
$\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}\alpha(\top a_{n})=\alpha(\top
a_{n}\llbracket\mathtt{t_{0}}\rrbracket_{u})=\alpha(\top a_{n+1})$. Finally,
the inductive hypothesis yields $\forall
n\in\mathbb{N}.\;\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a_{n}]\;\mathtt{t_{0}}\;[a_{n+1}]$.

We want to use the rule (limit) with postcondition
$\bigvee_{n\in\mathbb{N}}a_{n}$. To do so, we need to show two additional
facts: 1) the disjunction exists 2) $\top$ distributes over the disjunction.
1) holds as
$a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{*}=\bigvee_{n\in\mathbb{N}}a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}=\bigvee_{n\in\mathbb{N}}a_{n}$,
where the first equality holds by ∗-continuity. By ∗-continuity we have that
$\top
a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{*}=\bigvee_{n\in\mathbb{N}}\top
a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}=\bigvee_{n\in\mathbb{N}}\top
a_{n}$ and $\top
a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{*}=\top\bigvee_{n\in\mathbb{N}}a_{0}(\llbracket\mathtt{t_{0}}\rrbracket_{u})^{n}=\top\bigvee_{n\in\mathbb{N}}a_{n}$,
thus implying $\bigvee_{n\in\mathbb{N}}\top
a_{n}=\top\bigvee_{n\in\mathbb{N}}a_{n}$. Finally, by (limit) we obtain the
result
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t_{0}^{*}}\;[a\llbracket\mathtt{t_{0}^{*}}\rrbracket_{u}]$.
∎

Let us describe an example of derivation in $\operatorname{LCTK}_{A}$.

###### Example 5.6

Consider a relational KAT $K=\wp({\mathbb{Z}}\times{\mathbb{Z}})$ on the set
of integers $\mathbb{Z}$, where $\mathbf{1}_{K}\triangleq\\{(z,z)\mid
z\in\mathbb{Z}\\}$ and $\mathbf{0}_{K}\triangleq\varnothing$. Notice that
${\mathbb{Z}}\times{\mathbb{Z}}\in K$ is the top element $\top$ of $K$,
meaning that $K$ is a TopKAT. Let us consider a language with primitive
actions $\Sigma=\\{\mathtt{x:=x+1}\\}$ and primitive tests $B=\\{\mathtt{x\geq
0},\mathtt{x<0}\\}$. The evaluation function ${u:\Sigma\cup B\rightarrow K}$
is defined as expected by the following relations:

$\displaystyle u(\mathtt{x:=x+1})\triangleq\\{(z,z+1)\mid z\in\mathbb{Z}\\},$
$\displaystyle u(\mathtt{x\geq 0})\triangleq\\{(z,z)\mid z\in\mathbb{Z},z\geq
0\\},$ $\displaystyle u(\mathtt{x<0})\triangleq\\{(z,z)\mid
z\in\mathbb{Z},z<0\\}.$

Consider the following sign abstraction
$\operatorname{Sign}\triangleq\\{{\mathbb{Z}},{\mathbb{Z}}_{\leq
0},{\mathbb{Z}}_{\neq 0},{\mathbb{Z}}_{\geq
0},{\mathbb{Z}}_{<0},{\mathbb{Z}}_{=0},{\mathbb{Z}}_{>0},\varnothing\\}$ of
$\wp(\mathbb{Z})$, whose abstraction and concretization maps are
straightforward. Let us verify that the program

${\mathtt{r}\equiv\big{(}(\mathtt{x\geq
0})\cdot(\mathtt{x:=x+1})\big{)}^{*}\cdot(\mathtt{x<0})}$

does not terminate with precondition $p\triangleq\\{(0,0),(10,10)\\}$, i.e.,
we prove the specification $\operatorname{Spec}\triangleq\varnothing$. Let us
define the following auxiliary elements: $q\triangleq\\{(1,1),(11,11)\\}$,
${s\triangleq p+q}$, ${t_{\geq 0}\triangleq\\{(x,z)\mid
x\in\mathbb{Z},z\in{\mathbb{Z}}_{\geq 0}\\}}$, and observe that
$\operatorname{Sign}(t_{\geq 0})=t_{\geq 0}$.

The following local completeness conditions for the atoms hold:

$\displaystyle\alpha(\operatorname{Sign}(\top p)\llbracket\mathtt{x\geq
0}\rrbracket_{u})$ $\displaystyle=\alpha(t_{\geq 0}\llbracket\mathtt{x\geq
0}\rrbracket_{u})=\mathbb{Z}_{\geq 0}=\alpha(\top p\llbracket\mathtt{x\geq
0}\rrbracket_{u}),$ $\displaystyle\alpha(\operatorname{Sign}(\top
p)\llbracket\mathtt{x:=x+1}\rrbracket_{u})$ $\displaystyle=\alpha(t_{\geq
0}\llbracket\mathtt{x:=x+1}\rrbracket_{u})=\mathbb{Z}_{>0}=\alpha(\top
p\llbracket\mathtt{x:=x+1}\rrbracket_{u}),$
$\displaystyle\alpha(\operatorname{Sign}(\top
s)\llbracket\mathtt{x<0}\rrbracket_{u})$ $\displaystyle=\alpha(t_{\geq
0}\llbracket\mathtt{x<0}\rrbracket_{u})=\varnothing=\alpha(\top
s\llbracket\mathtt{x<0}\rrbracket_{u}).$

Moreover, we also have that:

$\displaystyle\top q$ $\displaystyle=\\{(x,z)\mid
x\in\mathbb{Z},z\in\\{1,11\\}\\}\leq\>t_{\geq 0}=\operatorname{Sign}(\top p).$

The following derivation shows that the triple
$[p]\;\mathtt{r}\;[\mathbf{0}_{K}]$ is provable in
$\operatorname{LCTK}_{\operatorname{Sign}}$:

$\mathbb{C}^{\operatorname{Sign}}_{p}(\llbracket\mathtt{x\geq
0}\rrbracket_{u})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{\operatorname{Sign}}[p]\;\mathtt{x\geq
0}\;[p]$
$\mathbb{C}^{\operatorname{Sign}}_{p}(\llbracket\mathtt{x:=x+1}\rrbracket_{u})$
(transfer)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{\operatorname{Sign}}[p]\;\mathtt{x:=x+1}\;[q]$
(seq)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{\operatorname{Sign}}[p]\;\mathtt{(x\geq
0)\cdot(x:=x+1)}\;[q]$ $\top q\leq\operatorname{Sign}(\top p)$ (iterate)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{\operatorname{Sign}}[p]\;\mathtt{\big{(}(x\geq
0)\cdot(x:=x+1)\big{)}^{*}}\;[s]$
$\mathbb{C}^{\operatorname{Sign}}_{s}(\llbracket\mathtt{x<0}\rrbracket_{u})$
(transfer)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{\operatorname{Sign}}[s]\;\mathtt{x<0}\;[\mathbf{0}_{K}]$
(seq)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{\operatorname{Sign}}[p]\;\mathtt{\big{(}(x\geq
0)\cdot(x:=x+1)\big{)}^{*}\cdot(x<0)}\;[\mathbf{0}_{K}]$

By Theorem 5.4, we have that $\top\mathbf{0}_{K}\subseteq\top
p\llbracket\mathtt{r}\rrbracket_{u}\subseteq\operatorname{Sign}(\top\mathbf{0}_{K})=\varnothing$,
meaning that the program does not terminate, and $\operatorname{Spec}$ is
satisfied as $\top
p\llbracket\mathtt{r}\rrbracket_{u}=\varnothing=\top\operatorname{Spec}$. ∎

###  5.3 Relationship with Under-Approximation Logic

We have shown in Section 3.6 that the backward-diamond formulation of
$\operatorname{LCK}$ generalizes $\operatorname{UL}$. The same can be done for
the TopKAT formulation. A TopKAT version of the $\operatorname{UL}$ proof
system has been already proposed in [34, Figure 6]. The reduction here
considered refers to such system, with the following minor differences:

  * •

We consider only propositional fragments of the logic, meaning that the rules
(assume) and (identity) are replaced by the following single (transfer) rule:

$\mathtt{c}\in\operatorname{Atom}$ (transfer)
$\vdash_{\operatorname{UL}}[a]\;\mathtt{c}\;[a\llbracket\mathtt{c}\rrbracket_{u}]$

  * •

The premises of the (consequence) rule in [34, Figure 6], $b\leq b^{\prime}$
and $c^{\prime}\leq c$, are relaxed to $\top b\leq\top b^{\prime}$ and $\top
c^{\prime}\leq\top c$. Notice that the former implies the latter. Furthermore,
the soundness proof of [34, Theorem 4] is not affected by this change, because
$(\top b^{\prime}\geq\top b\land\top c\geq\top c^{\prime}\land\top bp\geq
c)\Rightarrow\top b^{\prime}p\geq\top bp\geq\top c\geq\top c^{\prime}$, and,
by [34, Theorem 3], it holds that $\top b^{\prime}p\geq\top c^{\prime}$
entails $\top b^{\prime}p\geq c^{\prime}$.

  * •

The (limit) rules of $\operatorname{LCTK}_{A}$ and $\operatorname{UL}$ differ
on the distributivity condition. We assume that distributivity also holds in
$\operatorname{UL}$.

By instantiating to the trivial abstract domain $A_{tr}$, it turns out that
the two proof systems become equivalent.

######  Theorem 5.7 ($\operatorname{LCTK}_{A_{tr}}\equiv\operatorname{UL}$)

Let $K$ be a TopKAT∗. For any $a,b\in K$, $\mathtt{t}\in T_{\Sigma,B}$:

$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t}\;[b]\quad\Leftrightarrow\quad\vdash_{\operatorname{UL}}[a]\;\mathtt{t}\;[b].$

###### Proof

The $\Rightarrow$ direction can be shown as in Theorem 3.6. We focus instead
on the opposite direction.

$\Leftarrow$) The proof is by induction on the derivation tree of
$\vdash_{\operatorname{UL}}[a]\;\mathtt{t}\;[b]$. The rules of Table 1 are
immediate, meaning that only (empty),(choice),(disj),(iterate zero) and
(iterate non-zero) are left to prove. As in Theorem 3.6, we leverage the
completeness of the proof system and likewise, in order to prove that a triple
is valid, it is enough to show that condition (1) holds because (2) is
trivially true.

(empty) :
$\models^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t}\;[0]$ is
trivial since $\top\cdot 0=0\leq\top a\llbracket\mathtt{t}\rrbracket_{u}$ is
always true, therefore by completeness of $\operatorname{LCTK}_{A_{tr}}$,
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t}\;[0]$.

(choice) : By induction we have, without loss of generality,
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t_{1}}\;[b]$
and we need to show
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t_{1}+t_{2}}\;[b]$.
Notice that for any $\mathtt{t_{2}}\in T_{\Sigma,B}$,
$\models^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t_{2}}\;[0]$
because $\top\cdot 0=0\leq\top a\llbracket\mathtt{t_{2}}\rrbracket_{u}$,
therefore by completeness of $\operatorname{LCTK}_{A_{tr}}$
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t_{2}}\;[0]$.
Finally, (join) yields the result
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t_{1}+t_{2}}\;[b]$.

(disj) : By induction we have
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a_{1}]\;\mathtt{t}\;[b_{1}]$
and
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a_{2}]\;\mathtt{t}\;[b_{2}]$
and we need to show
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a_{1}+a_{2}]\;\mathtt{t}\;[b_{1}+b_{2}]$.
By soundness $\top b_{1}\leq\top a_{1}\llbracket\mathtt{t}\rrbracket_{u}$ and
$\top b_{2}\leq\top a_{2}\llbracket\mathtt{t}\rrbracket_{u}$, so that
$\top(b_{1}+b_{2})\leq\top(a_{1}+a_{2})\llbracket\mathtt{t}\rrbracket_{u}$.
Finally, by completeness we retrieve the result:
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a_{1}+a_{2}]\;\mathtt{t}\;[b_{1}+b_{2}]$.

(iterate zero) : By ($*$-unfold)
$\llbracket\mathtt{t^{*}}\rrbracket_{u}=(\llbracket\mathtt{t}\rrbracket_{u})^{*}\geq
1$, so that $\top a\llbracket\mathtt{t^{*}}\rrbracket_{u}\geq\top a$ and by
completeness
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t^{*}}\;[a]$.

(iterate non-zero) : By ($*$-unfold)
$\llbracket\mathtt{t^{*}}\rrbracket_{u}=(\llbracket\mathtt{t}\rrbracket_{u})^{*}\geq(\llbracket\mathtt{t}\rrbracket_{u})^{*}\llbracket\mathtt{t}\rrbracket_{u}=\llbracket\mathtt{t^{*}}\rrbracket_{u}\llbracket\mathtt{t}\rrbracket_{u}=\llbracket\mathtt{t^{*}\cdot
t}\rrbracket_{u}$. Thus, by hypothesis $\top b\leq\top
a\llbracket\mathtt{t^{*}\cdot t}\rrbracket_{u}\leq\top
a\llbracket\mathtt{t^{*}}\rrbracket_{u}$ and by completeness
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t^{*}}\;[b]$. ∎

In turn, the logical soundness and completeness of $\operatorname{UL}$ can be
retrieved as a consequence of those of $\operatorname{LCTK}$.

######  Corollary 3 ()

Under the same hypotheses of Theorem 5.7, the proof system $\operatorname{UL}$
is sound and complete, that is,
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]\;\Leftrightarrow\;\>\models_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]$.

###### Proof

$\displaystyle\vdash_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]$
$\displaystyle\Leftrightarrow\qquad\textrm{[by Theorem
\ref{thm:lctk_ul_equiv}]}$
$\displaystyle\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]$
$\displaystyle\Leftrightarrow\qquad\textrm{[by Theorems \ref{thm:lsound_top},
\ref{thm:lcompl_top}]}$
$\displaystyle\models^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]$
$\displaystyle\Leftrightarrow$
$\displaystyle\models_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]$ ∎

##  6 Incorrectness Logic in TopKAT

In Section 5 we proposed an alternative formulation of local completeness
logic based on a TopKAT. Here, we take a similar path as in Section 4 in
adding support for abnormal termination. Like in the modal formulation, each
language term is interpreted as a pair of KAT elements, meaning that the
interpretation function has signature
$\llbracket\mathtt{\cdot}\rrbracket_{u}:T_{\Sigma,B}\rightarrow(K\times K)$
and is defined inductively as in (30). Following the approach of Section 5 we
consider an element $\top pa$ as a proxy for the strongest postcondition and
in particular we have two such elements corresponding to, resp., normal and
abnormal termination: $\top
p{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}}$ and $\top
p{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}$.

The abstract semantic is a function of type
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}:T_{\Sigma,B}\rightarrow(A\rightarrow(A\times
A))$, where $A$ is a top Kleene abstract domain. As usual it is defined
inductively, with base case $\mathtt{a}\in\operatorname{Atom}$ defined as

$\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}p^{\sharp}\triangleq\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}:\alpha(\gamma(p^{\sharp}){\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{a}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}})},\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}:\alpha(\gamma(p^{\sharp}){\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{a}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})}$

and the inductive cases as in (33). It turns out that if $K$ is a TopKAT∗ then
the abstract semantic is sound and monotone.

###  6.1 Local completeness incorrectness logic on TopKAT

The proof system $\operatorname{LCIL}$ can be adapted to the TopKAT framework
as follows. Let $A$ be a top Kleene abstract domain on a TopKAT∗ $K$ and a
language $T_{\Sigma,B}$. If $a,b\in K$ and $\mathtt{t}\in T_{\Sigma,B}$, then

  * •

The triple
$[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}$
is valid (1) $\top b\leq\top
a{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}}$, and (2)
${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}}\alpha(\top a)=\alpha(\top b)=\alpha(\top
a{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}})$.

  * •

The triple
$[a]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}$
is valid (1) $\top c\leq\top
a{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}$, and (2)
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(\top a)=\alpha(\top c)=\alpha(\top
a{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})$.

  * •

A triple
$[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}$
is valid if both
$[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}$
and
$[a]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}$
are valid. In particular, if $b=c$ then the triple
$[a]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:b]}$
is valid.

The proof system, denoted $\operatorname{LCTIL}_{A}$, has the same rules as
$\operatorname{LCIL}_{A}$ in Figure 3 except for the rules (transfer) and
(relax), modified as follows:

$\mathtt{c}\in\operatorname{Atom}$
$\mathbb{C}^{A}_{a}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{c}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}})$
$\mathbb{C}^{A}_{a}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{c}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{c}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:a{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{c}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok
}}}}}]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:a{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{c}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}]}$

$\top a^{\prime}\leq\top a\leq A(\top
a^{\prime})\quad\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a^{\prime}]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:b^{\prime}]}\quad\top
b\leq\top b^{\prime}\leq A(\top b)$ (relax)
$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A}[a]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:b]}$

Moreover, for the rule (limit) we assume that the infinitary disjunction
exists and that $\top$ distributes over $\bigvee_{n\in\mathbb{N}}a_{n}$.
Observe that these additional conditions are the same as (a) for the TopKAT
formulation of the local completeness logic.

It turn out that $\operatorname{LCTIL}_{A}$ is logically sound and complete.

######  Theorem 6.1 (Logical Soundness of $\operatorname{LCTIL}_{A}$)

The triples provable in $\operatorname{LCTIL}_{A}$ are valid.

###### Proof

Analogous to the proof of Theorem 4.2. ∎

######  Theorem 6.2 (Logical completeness of $\operatorname{LCTIL}_{A}$)

Assume that the atoms in $\mathtt{t}\in T_{\Sigma,B}$ are globally complete,
i.e., for all $\mathtt{a}\in\operatorname{Atom}$,
$\mathbb{C}^{A}({\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{a}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}})$ and
$\mathbb{C}^{A}({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{a}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})$. If
$[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}$
is valid,then it is provable in $\operatorname{LCTIL}_{A}$.

###### Proof

It is easy to check that
${\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}}\alpha(\top a)=\alpha(\top
a{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}
ok }}}}})$ and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(\top a)=\alpha(\top
a{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})$, as in Lemmas 5 and 7. Then we can proceed as in Theorem 4.3 to
obtain the result. ∎

###  6.2 Relationship with Incorrectness logic

In Section 4.1 and 5.3 we have shown that the modal formulation of
$\operatorname{LCIL}$ generalizes $\operatorname{IL}$ and
$\operatorname{LCTK}$ generalizes $\operatorname{UL}$. Likewise, it is
possible to show that $\operatorname{LCTIL}$ generalizes $\operatorname{IL}$.
A TopKAT formulation of the $\operatorname{IL}$ proof system was already
proposed in [34, Figure 4]. We refer to such system for the proposed
reduction, with the same minor changes that we discussed in Section 5.3,
namely: 1) we consider only propositional fragments of the logic, 2) the
premises of (consequence) are relaxed to $\top b\leq\top b^{\prime}$ and $\top
c^{\prime}\leq\top c$, 3) we assume that the distributivity condition is
satisfied also in $\operatorname{IL}$.

Similarly to the reductions already proposed in this paper, we let $A=A_{tr}$,
where $A_{tr}$ is the trivial abstract domain.

######  Theorem 6.3 ($\operatorname{LCTIL}\equiv\operatorname{IL}$)

Let $K$ be a TopKAT∗. For any $a,b\in K$, $\mathtt{t}\in T_{\Sigma,B}$,

$\vdash^{{\scriptscriptstyle\mathrm{TK}}}_{A_{tr}}[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}\quad\Leftrightarrow\quad\vdash_{\operatorname{IL}}[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}$

###### Proof

Analogous to the proof of Theorem 4.5. ∎

Finally, we can retrieve the logical soundness and completeness of
$\operatorname{IL}$ as a consequence of those of $\operatorname{LCTIL}$.

###### Corollary 4

Under the hypothesis of Theorem 6.3 the proof system $\operatorname{IL}$ is
logically sound and complete, that is,
$\vdash_{\operatorname{IL}}[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}\;\Leftrightarrow\;\models_{\operatorname{IL}}[a]\;\mathtt{t}\;{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@cmyk@stroke{1}{0}{1}{0}\pgfsys@color@cmyk@fill{1}{0}{1}{0}[\mathbf{ok}:b]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:c]}$.

##  7 Conclusion

This work has shown that the abstract interpretation-based local completeness
logic introduced in [5] can be generalized to and interpreted in Kleene
algebra with tests. In particular, we proved that this can be achieved both
for KATs extended with a modal backward diamond operator playing the role of
strongest postcondition, and for KATs endowed with a top element. Our results
generalize both the modal [24] and top [34] KAT approaches that encode Hoare
correctness and O’Hearn incorrectness logic using different classes of KATs.
In particular, our KAT-based logic leverages an abstract interpretation of
KAT, a problem that was not studied so far.

Our plan for future work includes, but is not limited to, the following
questions.

  * •

For a KAT with top $\top$, following the technical idea underlying the
approach by Zhang et al. [34], we defined an abstract domain as an
approximation of all the algebraic elements of type $\top\cdot a$, where $a$
is any element of the KAT (cf. Definition 5.2). Although this definition
technically works, it is somehow artificial, because the elements $\top\cdot
a$ do not carry a clear intuitive meaning. As an interesting future task, we
would like to characterize under which conditions an element $\top\cdot a$
coincides with $\top\cdot p$ for some test
$p\in\operatorname{\mathsf{test}}(K)$, and if such test $p$ is unique.

  * •

This work is a first step towards an _algebraic and equational approach to
abstract interpretation_. We envisage that the reasoning made by an abstract
interpreter of programs could be made purely equational within a KAT equipped
with a suitable collection of axioms. The ambition would be to conceive a
notion of _abstract Kleene algebra_ (AKA) making this slogan true: _AKA is for
the abstract interpretation of programs what KAT is for concrete
interpretation of programs_.

#### Acknowledgements.

Francesco Ranzato has been partially funded by the _Italian Ministry of
University and Research_ , under the PRIN 2017 project no. 201784YSZ5
“AnalysiS of PRogram Analyses (ASPRA)”, by _Facebook Research_ , under a
“Probability and Programming Research Award”, and by an _Amazon Research
Award_ for “AWS Automated Reasoning”.

## References

  * [1] Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 113–126. POPL ’14, ACM (2014). https://doi.org/10.1145/2535838.2535862
  * [2] Antoine Miné.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang., 4(3–4):120–372, dec 2017. https://doi.org/10.1561/2500000034
  * [3] Beckett, R., Greenberg, M., Walker, D.: Temporal NetKAT. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016. pp. 386–401. ACM (2016). https://doi.org/10.1145/2908080.2908108
  * [4] Bruni, R., Giacobazzi, R., Gori, R., Garcia-Contreras, I., Pavlovic, D.: Abstract extensionality: on the properties of incomplete abstract interpretations. Proc. ACM Program. Lang. 4(POPL), 28:1–28:28 (2020). https://doi.org/10.1145/3371096
  * [5] Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: A Logic for Locally Complete Abstract Interpretations. In: Proceedings 36th ACM/IEEE Symposium on Logic in Computer Science (LICS 2021). pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470608
  * [6] Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: Abstract interpretation repair. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 426–441. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3519939.3523453
  * [7] Cohen, E., Kozen, D., Smith, F.: The complexity of Kleene algebra with tests. Tech. rep., Cornell University, USA (1996), https://www.cs.cornell.edu/~kozen/Papers/ckat
  * [8] Conway, J.: Regular Algebra and Finite Machines. Chapman and Hall mathematics series, Dover Publications (2012)
  * [9] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1977). pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973
  * [10] Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1979). pp. 269–282. ACM (1979). https://doi.org/10.1145/567752.567778
  * [11] Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Logic 7(4), 798–833 (oct 2006). https://doi.org/10.1145/1183278.1183285
  * [12] Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (Apr 1979). https://doi.org/10.1016/0022-0000(79)90046-1
  * [13] Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. pp. 343–355. ACM (2015). https://doi.org/10.1145/2676726.2677011
  * [14] Giacobazzi, R., Ranzato, F., Scozzari., F.: Making abstract interpretation complete. Journal of the ACM 47(2), 361–416 (March 2000). https://doi.org/10.1145/333979.333989
  * [15] Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. pp. 261–273 (2015). https://doi.org/10.1145/2676726.2676987
  * [16] Greenberg, M., Beckett, R., Campbell, E.: Kleene algebra modulo theories: A framework for concrete KATs. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 594–608. PLDI 2022, Association for Computing Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3519939.3523722
  * [17] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (oct 1969). https://doi.org/10.1145/363235.363259
  * [18] D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366–390, 1994. https://doi.org/10.1006/inco.1994.1037
  * [19] Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (May 1997). https://doi.org/10.1145/256167.256195
  * [20] Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Logic 1(1), 60–76 (jul 2000). https://doi.org/10.1145/343369.343378
  * [21] Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: Proceedings 10th International Workshop on Computer Science Logic, CSL 1996, Annual Conference of the EACSL. Lecture Notes in Computer Science, vol. 1258, pp. 244–259. Springer (1996). https://doi.org/10.1007/3-540-63172-0_43
  * [22] Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O’Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6(OOPSLA1) (apr 2022). https://doi.org/10.1145/3527325
  * [23] Mamouras, K.: Equational theories of abnormal termination based on kleene algebra. In: Proceedings 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017. Lecture Notes in Computer Science, vol. 10203, pp. 88–105 (2017). https://doi.org/10.1007/978-3-662-54458-7_6
  * [24] Möller, B., O’Hearn, P.W., Hoare, T.: On algebra of program correctness and incorrectness. In: Proceedings of the 19th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2021. Lecture Notes in Computer Science, vol. 13027, pp. 325–343. Springer (2021). https://doi.org/10.1007/978-3-030-88701-8_20
  * [25] Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science 351(2), 221–239 (Feb 2006). https://doi.org/10.1016/j.tcs.2005.09.069
  * [26] O’Hearn, P.W.: Incorrectness logic. Proceedings of the ACM on Programming Languages 4(POPL), 1–32 (Jan 2020). https://doi.org/10.1145/3371078
  * [27] Poskitt, C.M.: Incorrectness logic for graph programs. In: Proceedings of the 14th International Conference on Graph Transformation, ICGT 2021. Lecture Notes in Computer Science, vol. 12741, pp. 81–101. Springer (2021). https://doi.org/10.1007/978-3-030-78946-6_5
  * [28] Raad, A., Berdine, J., Dang, H., Dreyer, D., O’Hearn, P.W., Villard, J.: Local reasoning about the presence of bugs: Incorrectness separation logic. In: Proceedings 32nd International Conference on Computer Aided Verification, CAV 2020. Lecture Notes in Computer Science, vol. 12225, pp. 225–252. Springer (2020). https://doi.org/10.1007/978-3-030-53291-8_14
  * [29] Raad, A., Berdine, J., Dreyer, D., O’Hearn, P.W.: Concurrent incorrectness separation logic. Proc. ACM Program. Lang. 6(POPL), 1–29 (2022). https://doi.org/10.1145/3498695
  * [30] Ranzato, F.: Complete abstractions everywhere. In: Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013. Lecture Notes in Computer Science, vol. 7737, pp. 15–26. Springer (2013). https://doi.org/10.1007/978-3-642-35873-9_3
  * [31] Smolka, S., Eliopoulos, S.A., Foster, N., Guha, A.: A fast compiler for NetKAT. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015. pp. 328–341. ACM (2015). https://doi.org/10.1145/2784731.2784761
  * [32] Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets Scott: Semantic foundations for probabilistic networks. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. p. 557–571. POPL 2017, ACM (2017). https://doi.org/10.1145/3009837.3009843
  * [33] Yan, P., Jiang, H., Yu, N.: On incorrectness logic for quantum programs. Proc. ACM Program. Lang. 6(OOPSLA1) (apr 2022). https://doi.org/10.1145/3527316
  * [34] Zhang, C., de Amorim, A.A., Gaboardi, M.: On Incorrectness Logic and Kleene Algebra with Top and Tests. Proceedings of the ACM on Programming Languages 6(POPL), 1–30 (Jan 2022). https://doi.org/10.1145/3498690