11institutetext: Dipartimento di Matematica, University of Padova, Italy

# Local Completeness Logic on Kleene Algebra with Tests

Marco Milanese  Francesco Ranzato

###### Abstract

Local Completeness Logic (LCL) has been put forward as a program logic for
proving both the correctness and incorrectness of program specifications. LCL
is an abstract logic, parameterized by an abstract domain that allows
combining over- and under-approximations of program behaviors. It turns out
that LCL instantiated to the trivial singleton abstraction boils down to
O’Hearn incorrectness logic, which allows us to prove the presence of program
bugs. It has been recently proved that suitable extensions of Kleene algebra
with tests (KAT) allow representing both O’Hearn incorrectness and Hoare
correctness program logics within the same equational framework. In this work,
we generalize this result by showing how KATs extended either with a modal
diamond operator or with a top element are able to represent the local
completeness logic LCL. This is achieved by studying how these extended KATs
can be endowed with an abstract domain so as to define the validity of
correctness/incorrectness LCL triples and to show that the LCL proof system is
logically sound and, under some hypotheses, complete.

###### Keywords:

Local Completeness Logic Incorrectness Logic Complete Abstract Interpretation
Kleene Algebra with Tests.

##  1 Introduction

Kleene algebra [8] with tests (KAT) [19] allows an equational reasoning on
programs and their properties. Programs are modeled as elements of a KAT, so
that their properties can be algebraically derived through the general
equational theory of KATs. KATs feature sound, complete, and decidable
equational theories and have found successful applications in several
different contexts, most notably in network programming [1, 32, 3, 13, 31].
The foundational study of Kozen [20] has shown that the reasoning of Hoare
correctness logic [17] can be encoded and formulated equationally within a
KAT. Later work by Desharnais, Möller and Struth [11, 25] extended KAT with a
domain (KAD) to express the modal operators of propositional dynamic logic
[12], thus enabling a more natural way of reasoning through a map from actions
to propositions. The expressive power of KAD has been recently substantiated
by Möller, O’Hearn and Hoare [24], who have shown how to encode both Hoare
[17] correctness and O’Hearn [26] incorrectness program logics in a unique
class of KAD where a backward diamond modality is exploited to encode
strongest postconditions. Furthermore, very recently, Zhang, De Amorim and
Gaboardi [34, Theorem 1] have shown that O’Hearn incorrectness logic cannot be
formulated within a conventional KAT, but, at the same time, a full fledged
modal KAT is not needed. In fact, [34] proves that a KAT including a greatest
element, called TopKAT, is capable to encode both Hoare and O’Hearn logic in a
purely equational fashion. Moreover, [34] provides a PSPACE algorithm to
decide TopKAT equality, based on a reduction to Cohen et al. [7]’s algorithm
for KAT.
This stream of works made it possible to reason equationally on both program
correctness and incorrectness in the same algebraic framework. For example, in
the KAD framework where a backward diamond modality
$\boldsymbol{\langle}a\boldsymbol{|}p$ plays the role of strongest
postcondition of a KAT element $a$ (viz., a program) for a KAT test $p$ (viz.,
a precondition), the validity of a Hoare correctness triple
$\\{p\\}\,a\,\\{q\\}$ is determined by the inequality
$\boldsymbol{\langle}a\boldsymbol{|}p\leq q$, while the validity of an O’Hearn
incorrectness triple $[p]\;\mathtt{\text{$a$}}\;[q]$ boils down to
$q\leq\boldsymbol{\langle}a\boldsymbol{|}p$. Moreover, if a KAT test $s$ plays
the role of specification for a program $a$ and a Hoare triple
$\\{p\\}\,\text{$a$}\,\\{q\\}$ is provable, then $a$ can be proved correct
through the inequality $q\leq s$. Vice versa, if
$[p]\;\mathtt{\text{$a$}}\;[q]$ is a provable incorrectness triple, then
incorrectness of $a$ can be verified as $q\leq\lnot s$.

##### The Problem.

Recently, Bruni et al. [5] put forward a novel program logic, called local
completeness logic $\operatorname{LCL}$, which is parameterized by an abstract
domain [9, 10] of program stores and simultaneously combines over- and under-
approximations of program behaviours. This program logic leverages the notion
of _locally complete_ abstract interpretation, meaning that the abstract
interpretation of atomic program commands, such as variable assignments and
Boolean guards, is complete (i.e. with no false alarm) _locally_ on the
preconditions, as opposed to standard completeness [14, 30] which must be
satisfied _globally_ for all the preconditions. While a global completeness
program logic was proposed in [15], Bruni et al. [5] design a proof system for
inferring that a program analysis is locally complete. It turns out [5,
Section VI] that the instantiation of this $\operatorname{LCL}$ program logic
to the trivial store abstraction with a unique “don’t know” value abstracting
any concrete store property, boils down to O’Hearn incorrectness logic [26].
Moreover, Bruni et al. [6] also show that abstract interpretations can be made
locally complete through minimal domain refinements that repair the lack of
local completeness in a given program analysis.
In the original definition of $\operatorname{LCL}$ in [5] program properties
are represented as elements of a concrete domain $C$ and program semantics as
functions of type $C\rightarrow C$. Although straightforward, this approach
determines a specific type of program semantics. Vice versa, by exploiting a
KAT, program properties are represented as tests and programs as generic
elements of the KAT. Hence, a KAT based formulation becomes agnostic w.r.t.
the underlying semantics and can therefore admit multiple different models of
computation (e.g., trace-based semantics, or even models not related to
program semantics as shown by the language-theoretic example in Section 3.5).
Furthermore, KAT is a particularly suitable formalism for compositionally
reasoning on programs as all its basic composition operations on programs
(concatenation, choice and Kleene iteration) are directly modeled within the
algebra: this allows us to represent composite programs and tests as elements
of the KAT and, in particular, to check for their equality and inclusion
directly in the algebra. Thus, following the KAT-based model of incorrectness
logic advocated by Möller, O’Hearn and Hoare [24], this paper pushes forward
this line of work by studying an algebraic formulation of $\operatorname{LCL}$
program logic, with the objective of showing that there is no need to leverage
particular semantic properties of programs to reason on their local
completeness.

##### Contributions.

In this work, we show that the local completeness logic $\operatorname{LCL}$
can be made fully algebraic in a suitable KAT, yet preserving all its
noteworthy logical properties proved in [5]. For this purpose we show that:

  * •

Our proof systems are logically sound and complete (likewise [5], completeness
needs some additional hypotheses).

  * •

By instantiating the algebraic version of the $\operatorname{LCL}$ logic to
the trivial domain abstracting any concrete value to “don’t know” we exactly
obtain O’Hearn incorrectness program logic [26], thus retrieving its logical
soundness and completeness as consequences of our results.

  * •

Triples of O’Hearn incorrectness logic carry two postconditions, corresponding
to normal and erroneous program termination. While the original local
completeness logic $\operatorname{LCL}$ in [5] only considers normal
termination, we propose a generalization that also supports erroneous
termination. Moreover, we use the KAD construction of [24] to generalize our
logical soundness and completeness results to incorrectness triples.

In particular, we study two different formulations of $\operatorname{LCL}$
given: (1) in a KAD, the KAT model used in [24], and (2) in a TopKAT, the KAT
model employed in [34]. In both frameworks, we put forward a suitable notion
of abstract domain of KAT that, correspondingly, induces a sound abstract
semantics for KAT programs (i.e., KAT terms). Our local completeness logic on
KAT, called $\operatorname{LCK}$, turns out to be logically sound w.r.t. this
abstract semantics, meaning that a provable $\operatorname{LCK}$ triple
$[p]\;\mathtt{\text{$a$}}\;[q]$ for an abstract domain $A$ on a KAT $K$
satisfies:

  1. (i)

$q$ is below the strongest postcondition in $K$ of the program term $a$ for
the precondition $p$;

  2. (ii)

the program term $a$ is locally complete for the precondition $p$ in the
abstract domain $A$;

  3. (iii)

the approximations in $A$ of $q$ and of the strongest postcondition of $a$ for
$p$ coincide.

##  2 Background on Kleene Algebra with Tests

A Kleene algebra with tests (KAT) is a purely algebraic structure that
provides an elegant equational framework for program reasoning. A KAT consists
of actions, playing the role of programs, and tests, interpreted as
pre/postconditions and Boolean guards. KAT elements can be combined with three
basic operations: nondeterministic choice $a_{1}+a_{2}$, sequential
composition $a_{1};a_{2}$, and Kleene iteration $a^{*}$. A standard model of
KAT used to represent computations is the relational model, in which KAT
elements are binary relations on some set, thus modeling programs as a
relation between input and output states. Further models of KAT include
regular languages over a finite alphabet, square matrices over another Kleene
algebra, and Kleene algebra modulo theories [16]. In the following, we briefly
recall some basics of KAT. For more details, the reader is referred to [8, 19,
11].

An _idempotent-semiring_ (_i-semiring_) is a tuple $(A,+,\cdot,0,1)$ where:
(1) $(A,+,0)$ is a commutative monoid with an idempotent addition, i.e., for
all $a\in A$, $a+a=a$; (2) $(A,\cdot,1)$ is a monoid, where the multiplication
symbol $\cdot$ is often omitted, such that, for any $a\in A$, $0\cdot a=a\cdot
0$; (3) multiplication distributes over addition (in both arguments). In an
i-semiring $A$, the relation $a\leq
b\stackrel{{\scriptstyle{\mbox{\tiny$\vartriangle$}}}}{{\Leftrightarrow}}a+b=b$
is a partial order, referred to as the natural ordering, that we will
implicitly use throughout the paper. Note that the addition $+$ is the join
w.r.t. this natural ordering.

A _test-semiring_ is a tuple
$(A,\operatorname{\mathsf{test}}(A),+,\cdot,\lnot,0,1)$ where: (1)
$(A,+,\cdot,0,1)$ is an i-semiring; (2)
$\operatorname{\mathsf{test}}(A)\subseteq A$, and
$(\operatorname{\mathsf{test}}(A),\lor,\land,\lnot,0,1)$ is a Boolean
subalgebra of $A$ with greatest element $1$ and least element $0$, complement
$\lnot$, where the meet $\land$ and join $\lor$ of the Boolean algebra
$\operatorname{\mathsf{test}}(A)$ coincide, resp., with multiplication $\cdot$
and addition $+$.

A _Kleene algebra_ is a tuple $(K,+,\cdot,\mathord{{}^{*}},0,1)$ where: (1)
$(K,+,\cdot,0,1)$ is an i-semiring; (2) $(\cdot)^{*}:K\rightarrow K$ is a
unary operation, called Kleene star or iteration, satisfying the following
conditions:

$\displaystyle 1+aa^{*}\leq a^{*}$ $\displaystyle 1+a^{*}a\leq a^{*}$
($*$-unfold) $\displaystyle b+ac\leq c\Rightarrow a^{*}b\leq c$ $\displaystyle
b+ca\leq c\Rightarrow ba^{*}\leq c$ ($*$-induction)

######  Definition 2.1 (KAT [19])

A _Kleene algebra with tests_ (_KAT_) is a two-sorted algebra
$(K,\operatorname{\mathsf{test}}(K),$ $+,\cdot,\mathord{{}^{*}},$ $\lnot,0,1)$
such that $(K,\operatorname{\mathsf{test}}(K),+,\cdot,\lnot,0,1)$ is a test-
semiring and $(K,+,\cdot,\mathord{{}^{*}},0,1)$ is a Kleene algebra.

A KAT $K$ is _countably-test-complete_ (_CTC_) if any countable subset of
$\operatorname{\mathsf{test}}(K)$ admits least upper bound (lub).

A KAT is ∗-continuous, referred to as KAT∗, if it satisfies the following
condition: for all $a,b,c\in K$, $ab^{*}c=\bigvee_{n\in\mathbb{N}}ab^{n}c$
(this equation implicitly assumes that the lub
$\bigvee_{n\in\mathbb{N}}ab^{n}c$, w.r.t. the natural ordering of $K$,
exists).

A _relational KAT_ [21] on a carrier set $X$ is determined by a set
$K\subseteq\wp(X\times X)$ of binary relations on $X$ with tests
$\operatorname{\mathsf{test}}(K)\subseteq\wp(\\{(x,x)\mid x\in X\\})$, where
addition is union, multiplication is composition of relations, the additive
identity is the empty relation, the multiplicative identity is $\\{(x,x)\mid
x\in X\\}$, the Kleene star is the reflexive-transitive closure, and test
complement is set complementation w.r.t. the multiplicative identity.

Informally, a backward diamond
$\boldsymbol{\langle}\,\mathord{\cdot}\,\boldsymbol{|}\,\cdot\>$ on a KAT
allows us to compute strongest postconditions of programs, that is,
$\boldsymbol{\langle}a\boldsymbol{|}p$ can be interpreted as
$\mathsf{post}[a]p$.

######  Definition 2.2 (bdKAT [24])

A _backward-diamond KAT_ (_bdKAT_) is a two-sorted algebra $(K,$
$\operatorname{\mathsf{test}}(K),+,\cdot,\mathord{{}^{*}},\lnot,0,1,\boldsymbol{\langle}\boldsymbol{|})$
such that:

  1. (1)

$(K,\operatorname{\mathsf{test}}(K),+,\cdot,\mathord{{}^{*}},\lnot,0,1)$ is a
KAT;

  2. (2)

$\boldsymbol{\langle}\,\mathord{\cdot}\,\boldsymbol{|}\,\cdot:K\rightarrow(\operatorname{\mathsf{test}}(K)\rightarrow\operatorname{\mathsf{test}}(K))$
is a _backward-diamond_ operator satisfying the following conditions: for all
$a,b\in K$ and $p,q\in\operatorname{\mathsf{test}}(K)$,

$\displaystyle\boldsymbol{\langle}a\boldsymbol{|}p\leq q\Leftrightarrow pa\leq
aq$ (bd1)
$\displaystyle\boldsymbol{\langle}ab\boldsymbol{|}p=\boldsymbol{\langle}b\boldsymbol{|}(\boldsymbol{\langle}a\boldsymbol{|}p)$
(bd2)

∎

The following proposition summarizes few well-known operative properties of
the ${\boldsymbol{\langle}\cdot\boldsymbol{|}}$ operator. Such operator can be
defined using the codomain $\rho(\cdot)$ as
$\boldsymbol{\langle}a\boldsymbol{|}p=\rho(pa)$ (e.g., as in [25, Section 5])
and those properties are simply derived as a consequence of [11, Lemma 4.11].
On the other hand, in this paper we consider a (equivalent) direct
axiomatization of the backward-diamond; therefore for the sake of completeness
we provide a direct proof.

###### Proposition 1

Let
$(K,\operatorname{\mathsf{test}}(K),+,\cdot,^{*},\lnot,0,1,\boldsymbol{\langle}\boldsymbol{|})$
a backward-diamond KAT. For any $a,b\in K$ and
$p,q\in\operatorname{\mathsf{test}}(K)$, the following properties hold

$\displaystyle\boldsymbol{\langle}a+b\boldsymbol{|}p=\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p$
(1)
$\displaystyle\boldsymbol{\langle}a\boldsymbol{|}(p+q)=\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}a\boldsymbol{|}q$
(2) $\displaystyle a\leq
b\Rightarrow\boldsymbol{\langle}a\boldsymbol{|}p\leq\boldsymbol{\langle}b\boldsymbol{|}p$
(3) $\displaystyle p\leq
q\Rightarrow\boldsymbol{\langle}a\boldsymbol{|}p\leq\boldsymbol{\langle}a\boldsymbol{|}q$
(4) $\displaystyle\boldsymbol{\langle}s\boldsymbol{|}p=p\cdot s$ (5)
$\displaystyle
p+\boldsymbol{\langle}a\boldsymbol{|}\boldsymbol{\langle}a^{*}\boldsymbol{|}p\leq\boldsymbol{\langle}a^{*}\boldsymbol{|}p$
(6)

If in addition, $K$ satisfies the CTC condition,

$\boldsymbol{\langle}a^{*}\boldsymbol{|}p=\bigvee_{n\in\mathbb{N}}\boldsymbol{\langle}a^{n}\boldsymbol{|}p.$
(7)

###### Proof

(1): For any $p,q\in\operatorname{\mathsf{test}}(K)$ and $a\in K$

$\displaystyle pa\leq aq$ $\displaystyle\Rightarrow paq^{\prime}\leq
aqq^{\prime}\Rightarrow paq^{\prime}=0$ $\displaystyle paq^{\prime}=0$
$\displaystyle\Rightarrow pa=pa\cdot
1=pa(q+q^{\prime})=paq+paq^{\prime}=paq\Rightarrow pa\leq aq$

thus

$pa\leq aq\Leftrightarrow paq^{\prime}=0$ (8)

where $\lnot q$ is denoted with $q^{\prime}$. We have

$\displaystyle\boldsymbol{\langle}a+b\boldsymbol{|}p\leq q$
$\displaystyle\Leftrightarrow\textrm{[By (\ref{eqn:bdia1})]}$ $\displaystyle
p(a+b)\leq(a+b)q$ $\displaystyle\Leftrightarrow\textrm{[By
(\ref{eqn:claim_9})]}$ $\displaystyle p(a+b)q^{\prime}=0$
$\displaystyle\Leftrightarrow$ $\displaystyle paq^{\prime}+pbq^{\prime}=0$
$\displaystyle\Leftrightarrow$ $\displaystyle paq^{\prime}=0\land
pbq^{\prime}=0$ $\displaystyle\Leftrightarrow\textrm{[By
(\ref{eqn:claim_9})]}$ $\displaystyle pa\leq aq\land pb\leq bq$
$\displaystyle\Leftrightarrow\textrm{[By (\ref{eqn:bdia1})]}$
$\displaystyle\boldsymbol{\langle}a\boldsymbol{|}p\leq
q\land\boldsymbol{\langle}b\boldsymbol{|}p\leq q$
$\displaystyle\Leftrightarrow$
$\displaystyle\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p\leq
q$

Finally, since $q$ is arbitrary:

$\displaystyle\boldsymbol{\langle}a+b\boldsymbol{|}p\leq\boldsymbol{\langle}a+b\boldsymbol{|}p\Rightarrow\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p\leq\boldsymbol{\langle}a+b\boldsymbol{|}p$
$\displaystyle\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p\leq\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p\Rightarrow\boldsymbol{\langle}a+b\boldsymbol{|}p\leq\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p$

implying the claim
$\boldsymbol{\langle}a+b\boldsymbol{|}p=\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p$.

(2): Same as (1).

(3): By definition $a\leq b\Leftrightarrow a+b=b$, thus

$\boldsymbol{\langle}b\boldsymbol{|}p=\boldsymbol{\langle}a+b\boldsymbol{|}p\stackrel{{\scriptstyle(\ref{eqn:bdia_add_cmd})}}{{=}}\boldsymbol{\langle}a\boldsymbol{|}p+\boldsymbol{\langle}b\boldsymbol{|}p$

implying
$\boldsymbol{\langle}a\boldsymbol{|}p\leq\boldsymbol{\langle}b\boldsymbol{|}p$.

(4): Same as (3).

(5): Since $p,s\in\operatorname{\mathsf{test}}(K)$ and
$\operatorname{\mathsf{test}}(K)$ forms a boolean algebra $ps=sps$ and by
(bd1) $\boldsymbol{\langle}s\boldsymbol{|}p\leq ps$. Still by (bd1), $ps\leq
s\boldsymbol{\langle}s\boldsymbol{|}p\leq\boldsymbol{\langle}s\boldsymbol{|}p$,
implying $\boldsymbol{\langle}s\boldsymbol{|}p=ps$.

(6): The axiom ($*$-unfold) implies $1+a^{*}a\leq a^{*}$ so that

$\displaystyle 1+a^{*}a\leq a^{*}$ $\displaystyle\Rightarrow\textrm{[By
(\ref{eqn:bdia_isotony_cmd})]}$
$\displaystyle\boldsymbol{\langle}1+a^{*}a\boldsymbol{|}p\leq\boldsymbol{\langle}a^{*}\boldsymbol{|}p$
$\displaystyle\Rightarrow\textrm{[By (\ref{eqn:bdia_add_cmd})]}$
$\displaystyle\boldsymbol{\langle}1\boldsymbol{|}p+\boldsymbol{\langle}a^{*}a\boldsymbol{|}p\leq\boldsymbol{\langle}a^{*}\boldsymbol{|}p$
$\displaystyle\Rightarrow\textrm{[By (\ref{eqn:bdia_test})]}$ $\displaystyle
p+\boldsymbol{\langle}a^{*}a\boldsymbol{|}p\leq\boldsymbol{\langle}a^{*}\boldsymbol{|}p$
$\displaystyle\Rightarrow\textrm{[By (\ref{eqn:bdia2})]}$ $\displaystyle
p+\boldsymbol{\langle}a\boldsymbol{|}\boldsymbol{\langle}a^{*}\boldsymbol{|}p\leq\boldsymbol{\langle}a^{*}\boldsymbol{|}p.$

(7): The proof of this property can be found in [24, Lemma 3.3]. ∎

The axiom (bd1) is equivalent to requiring that
$\boldsymbol{\langle}a\boldsymbol{|}p$ is the least test in $K$ satisfying
$pa\leq aq$ (the original definition of Kleene algebra with domain in [11] is
of this form). Moreover, $pa\leq aq$ in (bd1) is equivalent to $pa=paq$ (see
[11, Lemma 3.4]). For the sake of completeness we provide a direct proof of
this fact.

######  Lemma 1 ()

Let
$(K,\operatorname{\mathsf{test}}(K),+,\cdot,\mathord{{}^{*}},\lnot,0,1,\boldsymbol{\langle}\boldsymbol{|})$
a bdKAT. For all $p\in\operatorname{\mathsf{test}}(K)$ and $a\in K$, (bd1)
holds iff $\boldsymbol{\langle}a\boldsymbol{|}p$ is the least (w.r.t. $\leq$)
${q\in\operatorname{\mathsf{test}}(K)}$ such that $pa=paq$.

###### Proof

First we show the equivalence between $pa\leq aq$ and $pa=paq$. Indeed:
${pa\leq aq}$ implies $pa=ppa\leq paq$ and $1\geq q$ implies $pa\geq paq$,
meaning that $pa=paq$. Viceversa if $pa=paq$, then $p\leq 1$ implies
$pa=paq\leq aq$.

We can show that (bd1) is equivalent to say that
$\boldsymbol{\langle}a\boldsymbol{|}p$ is the least
$q\in\operatorname{\mathsf{test}}(K)$ satisfying ${pa\leq aq}$ (which is
equivalent to $pa=paq$). In formulas the latter is

$\displaystyle pa$ $\displaystyle\leq a\boldsymbol{\langle}a\boldsymbol{|}p$
(9) $\displaystyle pa$ $\displaystyle\leq
aq\Rightarrow\boldsymbol{\langle}a\boldsymbol{|}p\leq q$ (10)

Assume (bd1). (10) is the direction $\Leftarrow$ of (bd1). (9) holds by
instantiating $q=\boldsymbol{\langle}a\boldsymbol{|}p$ in (bd1). Viceversa,
assume (9) and (10). (10) is the direction $\Leftarrow$ of (bd1). The other
direction holds because $pa\leq a\boldsymbol{\langle}a\boldsymbol{|}p\leq aq$.
∎

######  Definition 2.3 (TopKAT [23])

A _KAT with top_ (_TopKAT_) is a KAT $K$ that contains a largest element
$\top\in K$, that is, for all $a\in K$, $a\leq\top$. ∎

##  3 Local Completeness Logic in KAT

We investigate how the local completeness program logic $\operatorname{LCL}$
[5] can be interpreted on a KAT. To achieve this, we need to address the
following tasks:

  * •

To define a notion of abstract domain of a KAT, with the aim of abstracting
the set of program predicates, namely tests of a KAT;

  * •

To establish a concrete semantics and a corresponding sound abstract semantics
of programs on KATs;

  * •

To adapt the local completeness proof system to attain valid triples on a KAT;

  * •

To prove logical soundness and completeness w.r.t. a KAT of this new proof
system.

###  3.1 Program Properties in KAT

Program properties can be broadly classified as intensional and extensional.
The former relate to how programs are written, while the latter concern the
input-output relation of a program, i.e., its strongest postcondition
denotational semantics. Local completeness logic $\operatorname{LCL}$ relies
on an abstract interpretation of programs which crucially depends on
intensional properties of programs, meaning that even if two programs share
the same denotation, they could well have different abstract semantics. Thus,
we expect that an appropriate definition of abstract semantics based on a KAT
model should also be intensional. Given two elements $a$ and $b$ of a modal
bdKAT playing the role of programs, we therefore expect that their backward
diamond functions might coincide, i.e.
$\boldsymbol{\langle}a\boldsymbol{|}=\boldsymbol{\langle}b\boldsymbol{|}$,
even if $a$ and $b$ encode different programs, i.e. $a\neq b$. However, as
shown by the following remark for the basic relational model of KAT, it might
happen that for certain classes of KAT models the backward diamond
interpretation is injective.

In order to prove such result, we require an auxiliary Lemma to provide an
explicit formula for the $\boldsymbol{\langle}\cdot\boldsymbol{|}$ operator in
the special case of full set of tests (i.e.,
$\operatorname{\mathsf{test}}(K)=\wp(\\{(x,x)\mid x\in X\\})$).

###### Lemma 2

Let $K$ be a relational KAT on a set $X$ where
$\operatorname{\mathsf{test}}(K)=\wp(\\{(x,x)\mid x\in X\\})$. Then, for all
$a\in K$ and $p\in\operatorname{\mathsf{test}}(K)$,

$\boldsymbol{\langle}a\boldsymbol{|}p=\\{(y,y)\mid\exists x\in X.\;(x,x)\in
p,(x,y)\in a\\}$

###### Proof

We want to show that $\boldsymbol{\langle}a\boldsymbol{|}p$ exists and is
equal to

$s=\\{(y,y)\mid\exists x\in X.\;(x,x)\in p,(x,y)\in a\\}.$

Using the characterization of $\boldsymbol{\langle}a\boldsymbol{|}p$ of Lemma
1, we need to show that $s$ is the least $q\in\operatorname{\mathsf{test}}(K)$
satisfying $pa=paq$. In this context

$\displaystyle paq$ $\displaystyle=\\{(x,y)\mid(x,x)\in p,(x,y)\in a,(y,y)\in
q\\}$ $\displaystyle pa$ $\displaystyle=\\{(x,y)\mid(x,x)\in p,(x,y)\in a\\}$

First we show that $pa=pas$. Assume $(x,y)\in pa$, then by definition of $s$
it holds $(y,y)\in s$, meaning that $(x,y)\in pas$. This shows $pa\leq pas$,
the other inequality is immediate since $s\leq 1$ so that $pa\geq pas$.

Secondly we show that $s$ is the least such element. Assume by contradiction
that $\exists t\in\operatorname{\mathsf{test}}(K)$ satisfying $pa=pat$ and
$t<s$. Let $(y,y)\in s\setminus t$. By definition of $s$ exists $x\in X$ such
that $(x,x)\in p$ and $(x,y)\in a$, therefore $(x,y)\notin pat$ because $t$ is
a subidentity and $(y,y)\notin t$. This contradicts the hypothesis $pa=pat$. ∎

######  Proposition 2 ()

Let $K$ be a relational KAT on a set $X$ where
$\operatorname{\mathsf{test}}(K)=\wp(\\{(x,x)\mid x\in X\\})$. Then, for all
$a,b\in K$,
$\boldsymbol{\langle}a\boldsymbol{|}=\boldsymbol{\langle}b\boldsymbol{|}\;\Leftrightarrow\;a=b$.

###### Proof

The direction $\Leftarrow$ is trivial, because
$\boldsymbol{\langle}\cdot\boldsymbol{|}$ is a function on the first argument.
Instead, we focus on the $\Rightarrow$ direction.

Assume
$\boldsymbol{\langle}a\boldsymbol{|}=\boldsymbol{\langle}b\boldsymbol{|}$. If
$(x,y)\in a$, then by Lemma 2

$\boldsymbol{\langle}a\boldsymbol{|}\\{(x,x)\\}=\boldsymbol{\langle}b\boldsymbol{|}\\{(x,x)\\}\supseteq\\{(y,y)\\}$

This implies the existence of $z\in X$ such that $(z,z)\in\\{(x,x)\\}$ and
$(z,y)\in b$, but the only possibility is $z=x$ so that $(x,y)\in b$. By
symmetry we can obtain $(x,y)\in b\Rightarrow(x,y)\in a$.

Notice that we can be sure that
$\\{(x,x)\\}\in\operatorname{\mathsf{test}}(K)$ because of the hypothesis
$\operatorname{\mathsf{test}}(K)=\wp(\\{(x,x)\mid x\in X\\})$. ∎

This means that, at least for some fundamental KAT models, KAT elements are
equal iff they are extensionally equal, or, equivalently, they carry
exclusively extensional program properties. In this case, when a program is
encoded with a KAT element all the intensional properties are lost and it is
indistinguishable from any other program with the same denotational semantics.
Therefore, an abstract interpretation-based semantics can not be defined
directly on KAT elements.

###  3.2 KAT Language

As a consequence of the discussion in Section 3.1, the concrete semantics
cannot be directly defined on KAT elements. A solution is to define it on an
inductive language. Actually, in a language of programs, two elements are
equal iff they are syntactically equal, or, in other terms, if the
corresponding programs are written in the same way. This property makes a
language an ideal basis upon which a semantics can be defined, because this
brings the chance of depending on intensional properties.

A natural choice for defining this language of programs is the so-called _KAT
language_ , as originally defined by Kozen and Smith [21, Section 2.3],
because it contains all and only the operators of a KAT, so that the
interpretation of language terms as KAT elements is the most natural one. This
language is inductively defined from two disjoint sets of primitive actions
and tests through the basic elements/operations $0,1,+,\cdot,^{*}$ of KATs.
More precisely, given a set $\Sigma$ of primitive actions and a set $B$ of
primitive tests such that $\Sigma\cap B=\varnothing$, the corresponding _KAT
language_ $T_{\Sigma,B}$ of terms is defined as follows:

$\displaystyle\operatorname{Atom}\ni\mathtt{a}::=a\in\mathit{\Sigma}\mid
p\in\mathit{B}$ $\displaystyle T_{\Sigma,B}\ni\mathtt{t::=\mathtt{a}\mid 0\mid
1\mid t_{1}+t_{2}\mid t_{1}\cdot t_{2}\mid t^{*}}$

For simplicity, we assume that $\mathtt{0}$ and $\mathtt{1}$ are primitive
tests in $B$, so that $\mathtt{0},\mathtt{1}\in\operatorname{Atom}$. The
notation $\operatorname{Atom}(\mathtt{t})\subseteq\operatorname{Atom}$ will
denote the set of atoms occurring in a term $\mathtt{t}\in T_{\Sigma,B}$.
Notice that a KAT language $T_{\Sigma,B}$ is an equivalent representation of
the language of regular commands used in [26, 5] for their program logics.

Given a KAT $K$, an evaluation of atoms in $K$ is a mapping
$u:\operatorname{Atom}\rightarrow K$ such that $\mathtt{p}\in B\Rightarrow
u(\mathtt{p})\in\operatorname{\mathsf{test}}(K)$. An evaluation $u$ induces an
interpretation of terms
$\llbracket\mathtt{\cdot}\rrbracket_{u}:T_{\Sigma,B}\rightarrow K$, which is
inductively defined as expected:

$\displaystyle\llbracket\mathtt{a}\rrbracket_{u}\triangleq u(\mathtt{a})$
$\displaystyle\llbracket\mathtt{t_{1}+t_{2}}\rrbracket_{u}\triangleq\llbracket\mathtt{t_{1}}\rrbracket_{u}+\llbracket\mathtt{t_{2}}\rrbracket_{u}$
$\displaystyle\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{u}\triangleq\llbracket\mathtt{t_{1}}\rrbracket_{u}\cdot\llbracket\mathtt{t_{2}}\rrbracket_{u}$
$\displaystyle\llbracket\mathtt{t^{*}}\rrbracket_{u}\triangleq\llbracket\mathtt{t}\rrbracket_{u}^{*}$

In turn, the concrete semantic function

$\llbracket\mathtt{\cdot}\rrbracket^{K}:T_{\Sigma,B}\rightarrow\big{(}\operatorname{\mathsf{test}}(K)\rightarrow\operatorname{\mathsf{test}}(K)\big{)}$

models the strongest postcondition of a program, i.e. of a language term, for
a given precondition, i.e. a KAT test. This is therefore defined in terms of
the backward diamond of a bdKAT as follows:

$\displaystyle\llbracket\mathtt{t}\rrbracket^{K}p\triangleq\boldsymbol{\langle}\llbracket\mathtt{t}\rrbracket_{u}\boldsymbol{|}p.$
(11)

We will often use $\llbracket\mathtt{t}\rrbracket$ to denote a concrete
semantics, by omitting the superscript $K$ when it is clear from the context.

The construction of the concrete semantic leverages the backward-diamond (11)
and the interpretation $\llbracket\mathtt{\cdot}\rrbracket_{u}$, hence the
properties of Proposition 1 can be transferred to
$\llbracket\mathtt{\cdot}\rrbracket^{K}$. For completeness we summarize them
in the following:

$\displaystyle p\leq q\Rightarrow\llbracket\mathtt{t}\rrbracket
p\leq\llbracket\mathtt{t}\rrbracket q$ (12)
$\displaystyle\llbracket\mathtt{t_{1}+t_{2}}\rrbracket
p=\llbracket\mathtt{t_{1}}\rrbracket p+\llbracket\mathtt{t_{2}}\rrbracket p$
(13)
$\displaystyle\llbracket\mathtt{t}\rrbracket(p+q)=\llbracket\mathtt{t}\rrbracket
p+\llbracket\mathtt{t}\rrbracket q$ (14)
$\displaystyle\llbracket\mathtt{t_{1}\cdot t_{2}}\rrbracket
p=\llbracket\mathtt{t_{2}}\rrbracket\llbracket\mathtt{t_{1}}\rrbracket p$ (15)
$\displaystyle\llbracket\mathtt{t^{*}}\rrbracket
p=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket)^{n}p$ (16)
$\displaystyle
p+\llbracket\mathtt{t}\rrbracket\llbracket\mathtt{t^{*}}\rrbracket
p\leq\llbracket\mathtt{t^{*}}\rrbracket p$ (17)

###  3.3 Kleene Abstractions

An abstract domain is used in abstract interpretation for approximating store
properties, i.e., sets of program stores form the concrete domain, likewise in
our KAT model, the role of concrete domain is played by the set of tests
$\operatorname{\mathsf{test}}(K)$ of a KAT $K$, ordered by the natural
ordering induced by $K$.

######  Definition 3.1 (Kleene Abstract Domain)

A poset $(A,\leq_{A})$ is a _Kleene abstract domain_ of a bdKAT $K$ if:

  1. (i)

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

  2. (ii)

$A$ is countably-complete, i.e., any countable subset of $A$ admits a lub. ∎

The abstract semantic function
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}:T_{\Sigma,B}\rightarrow(A\rightarrow
A)$ defines how abstract preconditions are transformed into abstract
postconditions. Likewise store-based abstract interpretation, this abstract
semantics is inductively defined as follows:

$\displaystyle\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}p^{\sharp}\triangleq\alpha(\llbracket\mathtt{a}\rrbracket^{K}\gamma(p^{\sharp}))$
$\displaystyle\quad\llbracket\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\rrbracket_{A}^{\sharp}p^{\sharp}\triangleq\llbracket\mathtt{t_{\text{$1$}}}\rrbracket_{A}^{\sharp}p^{\sharp}+\llbracket\mathtt{t_{\text{$2$}}}\rrbracket_{A}^{\sharp}p^{\sharp}$
(18) $\displaystyle\llbracket\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\rrbracket_{A}^{\sharp}p^{\sharp}\triangleq\llbracket\mathtt{t_{\text{$2$}}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{\text{$1$}}}\rrbracket_{A}^{\sharp}p^{\sharp})$
$\displaystyle\quad\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}p^{\sharp}\triangleq\textstyle\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}p^{\sharp}$

We recall in the following Proposition few properties of Galois Insertion.
Proofs and a more in depth-presentation are available in [2].

###### Proposition 3

Let $(C,\leq_{C})\galois{\alpha}{\gamma}(A,\leq_{A})$ a Galois Insertion.

$\displaystyle\forall c_{1},c_{2}\in C.\;$ $\displaystyle
c_{1}\leq_{C}c_{2}\Rightarrow\alpha(c_{1})\leq_{A}\alpha(c_{2})$ (19)
$\displaystyle\forall a_{1},a_{2}\in A.\;$ $\displaystyle
a_{1}\leq_{A}a_{2}\Rightarrow\gamma(a_{1})\leq_{C}\gamma(a_{2})$ (20)
$\displaystyle\forall a_{1},a_{2}\in A.\;$ $\displaystyle a_{1}\neq
a_{2}\Rightarrow\gamma(a_{1})\neq\gamma(a_{2})$ (21) $\displaystyle\forall
c\in C.\;$ $\displaystyle c\leq_{C}\gamma(\alpha(c))$ (22)
$\displaystyle\gamma\comp\alpha\comp\gamma\comp\alpha=\gamma\comp\alpha$ (23)

It is worth remarking that condition (ii) of Definition 3.1 ensures that the
abstract semantics of the Kleene star in (LABEL:def:abs-sem) is well defined.
It turns out that $\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}$ is a sound
(and monotonic) abstract semantics.

######  Theorem 3.2 (Soundness of bdKAT Abstract Semantics)

Let $A$ be a Kleene abstraction of a CTC bdKAT $K$ and $T_{\Sigma,B}$ be a
language interpreted on $K$. For all $p^{\sharp},q^{\sharp}\in A$,
$p\in\operatorname{\mathsf{test}}(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(\llbracket\mathtt{t}\rrbracket^{K}p)\leq_{A}\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)$
(soundness)

###### Proof

Let us prove the first implication. The proof is by induction on the structure
of $\mathtt{t}\in T_{\Sigma,B}$.
($\mathtt{a}\in\operatorname{Atom}$) :

$\displaystyle\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}p^{\sharp}$
$\displaystyle=$
$\displaystyle\alpha(\llbracket\mathtt{a}\rrbracket\gamma(p^{\sharp}))$
$\displaystyle\leq\textrm{[isotony of
$\alpha(\cdot)$,$\gamma(\cdot)$,$\llbracket\mathtt{\cdot}\rrbracket$]}$
$\displaystyle\alpha(\llbracket\mathtt{a}\rrbracket\gamma(q^{\sharp}))$
$\displaystyle=$
$\displaystyle\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}q^{\sharp}$

($\mathtt{t_{1}+t_{2}}$) : By induction it holds
$\llbracket\mathtt{t_{i}}\rrbracket_{A}^{\sharp}p^{\sharp}\leq\llbracket\mathtt{t_{i}}\rrbracket_{A}^{\sharp}q^{\sharp}$
for $i\in\\{1,2\\}$

$\llbracket\mathtt{t_{1}+t_{2}}\rrbracket_{A}^{\sharp}p^{\sharp}=\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}p^{\sharp}+\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}p^{\sharp}\leq\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}q^{\sharp}+\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}q^{\sharp}=\llbracket\mathtt{t_{1}+t_{2}}\rrbracket_{A}^{\sharp}q^{\sharp}\
$

($\mathtt{t_{1}\cdot t_{2}}$) : By induction it holds
$\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}p^{\sharp}\leq\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}q^{\sharp}$
and also
$\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}p^{\sharp})\leq\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}q^{\sharp})$

$\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{A}^{\sharp}p^{\sharp}=\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}p^{\sharp}\leq\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}q^{\sharp}=\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{A}^{\sharp}q^{\sharp}$

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

$\forall n\in\mathbb{N}.\;p^{\sharp}\leq
q^{\sharp}\Rightarrow(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}p^{\sharp}\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}q^{\sharp}$
(24)

which can be shown by induction on $n$.
${(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{0}p^{\sharp}=p^{\sharp}\leq
q^{\sharp}=(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{0}q^{\sharp}}$
and for the inductive case:
$(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n+1}p^{\sharp}=\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}p^{\sharp}\leq\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}q^{\sharp}\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n+1}q^{\sharp}$.
Therefore

$\llbracket\mathtt{t_{0}^{*}}\rrbracket_{A}^{\sharp}p^{\sharp}=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}p^{\sharp}\stackrel{{\scriptstyle(\ref{eqn:claim_10})}}{{\leq}}\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}q^{\sharp}=\llbracket\mathtt{t_{0}^{*}}\rrbracket_{A}^{\sharp}q^{\sharp}$

Similarly, the soundness is proven by induction on the structure of
$\mathtt{t}\in T_{\Sigma,B}$.
($\mathtt{a}\in\operatorname{Atom}$) : By isotony of $\alpha(\cdot)$,
$\llbracket\mathtt{\cdot}\rrbracket$ and (22) we have

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

($\mathtt{t_{1}+t_{2}}$) : By additivity of
$\llbracket\mathtt{\cdot}\rrbracket$ and $\alpha(\cdot)$ we have

$\displaystyle\alpha(\llbracket\mathtt{t_{1}+t_{2}}\rrbracket p)$
$\displaystyle=\alpha(\llbracket\mathtt{t_{1}}\rrbracket
p+\llbracket\mathtt{t_{2}}\rrbracket p)$
$\displaystyle=\alpha(\llbracket\mathtt{t_{1}}\rrbracket
p)+\alpha(\llbracket\mathtt{t_{2}}\rrbracket p)$
$\displaystyle\leq\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)+\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)$
$\displaystyle=\llbracket\mathtt{t_{1}+t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)$

($\mathtt{t_{1}\cdot t_{2}}$) : By isotony of
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}$ we have

$\displaystyle\alpha(\llbracket\mathtt{t_{1}\cdot t_{2}}\rrbracket p)$
$\displaystyle=\alpha(\llbracket\mathtt{t_{2}}\rrbracket\llbracket\mathtt{t_{1}}\rrbracket
p)$
$\displaystyle\leq\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(\llbracket\mathtt{t_{1}}\rrbracket
p)$
$\displaystyle\leq\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)$
$\displaystyle=\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)$

($\mathtt{t_{0}^{*}}$) : In order to show the result we need an auxiliary
claim:

$\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(p)$
(25)

The proof is by induction on $n$. The base case holds as
$\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{0}p)=\alpha(p)=(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{0}\alpha(p)$
and similarly the inductive case as
$\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n+1}p)=\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n}\llbracket\mathtt{t_{0}}\rrbracket
p)\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(\llbracket\mathtt{t_{0}}\rrbracket
p)\leq(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}\alpha(p)=(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n+1}\alpha(p)$.
Therefore we have

$\displaystyle\alpha(\llbracket\mathtt{t_{0}^{*}}\rrbracket p)$
$\displaystyle=\textrm{[By (\ref{eqn:csema_star})]}$
$\displaystyle\alpha(\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)$
$\displaystyle=\textrm{[By additivity of $\alpha(\cdot)$]}$
$\displaystyle\bigvee_{n\in\mathbb{N}}\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)$
$\displaystyle\leq\textrm{[By (\ref{eqn:claim_1})]}$
$\displaystyle\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(p)$
$\displaystyle=$
$\displaystyle\llbracket\mathtt{t_{0}^{*}}\rrbracket_{A}^{\sharp}\alpha(p)$

Notice that the CTC condition on $K$ must hold in order to apply (16). ∎

###  3.4 Local Completeness Logic on bdKAT

Given a Kleene abstract domain $A$, we will slightly abuse notation by using

$A\triangleq\gamma\comp\alpha:\operatorname{\mathsf{test}}(K)\rightarrow\operatorname{\mathsf{test}}(K)$

as a function (indeed, this is the upper closure operator on tests induced by
the Galois insertion defining $A$). Let us recall the notions of global vs.
local completeness. If
$f:\operatorname{\mathsf{test}}(K)\rightarrow\operatorname{\mathsf{test}}(K)$
is any test transformer then:

  * •

$A$ is _globally complete_ for $f$, denoted $\mathbb{C}^{A}(f)$, iff $A\comp
f=A\comp f\comp A$;

  * •

$A$ is _locally complete_ for $f$ on a concrete test
$p\in\operatorname{\mathsf{test}}(K)$, denoted $\mathbb{C}^{A}_{p}(f)$, iff
$A\comp f(p)=A\comp f\comp A(p)$.

It is known [15] that global completeness is hard to achieve in practice, even
for simple programs. Moreover, a complete and compositional (i.e., inductively
defined on program structure) abstract interpretation is even harder to design
[4]. This motivated to study a local notion of completeness in abstract
interpretation [5] as a pragmatic and more attainable weakening of standard
global completeness.

In our local completeness logic on a Kleene algebra, a triple
$[p]\;\mathtt{t}\;[q]$, where $p$ and $q$ are tests and $\mathtt{t}$ is a
language term, will be valid when:

  1. (1)

$q$ is an under-approximation of the concrete semantics of $\mathtt{t}$ from a
precondition $p$;

  2. (2)

$A$ is locally complete for $\llbracket\mathtt{t}\rrbracket$ on the
precondition $p$;

  3. (3)

$q$ and $\llbracket\mathtt{t}\rrbracket p$ have the same over-approximation in
$A$.

######  Definition 3.3 (Triple Validity)

Let $K$ a CTC bdKAT, $A$ be a Kleene abstraction of $K$, and $T_{\Sigma,B}$ be
a KAT language interpreted on $K$. For all
$p,q\in\operatorname{\mathsf{test}}(K)$ and $\mathtt{t}\in T_{\Sigma,B}$, a
triple $[p]\;\mathtt{t}\;[q]$ is valid in $A$, denoted by
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$, if

  1. (i)

$q\leq_{K}\llbracket\mathtt{t}\rrbracket^{K}p$;

  2. (ii)

$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q)=\alpha(\llbracket\mathtt{t}\rrbracket^{K}p)$.
∎

The local completeness proof system in [5] can be adapted to our algebraic
framework, yielding the set of rules denoted by $\operatorname{LCK}_{A}$ in
Figure 1. The only syntactic difference concerns the usage of elements of
$\operatorname{\mathsf{test}}(K)$ as pre/postconditions and the language of
terms $T_{\Sigma,B}$ playing the role of programs.

$\mathtt{a}\in\Sigma\cup B$
$\mathbb{C}^{A}_{p}(\llbracket\mathtt{a}\rrbracket)$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{a}\;[\llbracket\mathtt{a}\rrbracket
p]$

$p^{\prime}\leq
p\leq\\!A(p^{\prime})\qquad\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p^{\prime}]\;\mathtt{t}\;[q^{\prime}]\qquad
q\leq q^{\prime}\leq\\!A(q^{\prime})$ (relax)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}}\;[r]$
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[r]\;\mathtt{t_{\text{$2$}}}\;[q]$
(seq)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\;[q]$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}}\;[q_{1}]$
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$2$}}}\;[q_{2}]$
(join)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\;[q_{1}+q_{2}]$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[r]$
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p+r]\;\mathtt{t^{*}}\;[q]$ (rec)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t^{*}}\;[q]$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$ $q\leq A(p)$
(iterate)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t^{*}}\;[p+q]$

Figure 1: Proof system $\operatorname{LCK}_{A}$.

It turns out that the logic $\operatorname{LCK}_{A}$ is logically sound (we
use “logical” soundness to avoid overloading the soundness of abstract
semantics).

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

If $\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$ then

  1. (i)

$q\leq_{K}\llbracket\mathtt{t}\rrbracket p$;

  2. (ii)

$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q)=\alpha(\llbracket\mathtt{t}\rrbracket
p)$.

###### Proof

The proof is adapted from [5, Theorem 5.5]. The first equality of (ii) is a
consequence of the first one, (i) and soundness:

$\alpha(q)\leq\alpha(\llbracket\mathtt{t}\rrbracket
p)\leq\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q)$

that implies $\alpha(q)=\alpha(\llbracket\mathtt{t}\rrbracket p)$. For this
reason we only need to prove
$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q)$.

The proof is on the structure of the derivation tree of
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$.

(transfer) : (i) is trivial, while (ii) is a consequence of the local
completeness axiom $\mathbb{C}_{p}^{A}(\llbracket\mathtt{a}\rrbracket)$,
$\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(\llbracket\mathtt{a}\rrbracket\gamma(\alpha(p)))\stackrel{{\scriptstyle\text{LC}}}{{=}}\alpha(\llbracket\mathtt{a}\rrbracket
p)=\alpha(q)$.

(relax) : By induction $q^{\prime}\leq\llbracket\mathtt{t}\rrbracket
p^{\prime}$ so that $q\leq q^{\prime}\leq\llbracket\mathtt{t}\rrbracket
p^{\prime}\leq\llbracket\mathtt{t}\rrbracket p$, implying (i). By hypothesis
we have $p^{\prime}\leq p\leq A(p^{\prime})$. By isotony of $\alpha(\cdot)$
and $\gamma(\cdot)$, and (23) we have that $A(p^{\prime})\leq A(p)\leq
A(A(p^{\prime}))=A(p^{\prime})$, which means $A(p^{\prime})=A(p)$. By the same
reasoning $A(q)=A(q^{\prime})$. By injectivity of $\gamma(\cdot)$ we have
$\alpha(p^{\prime})=\alpha(p)$ and ${\alpha(q^{\prime})=\alpha(q)}$. This
proves (ii).

(seq) : (i) holds by isotony of $\llbracket\mathtt{\cdot}\rrbracket$ and by
induction $q\leq\llbracket\mathtt{t_{2}}\rrbracket
r\leq\llbracket\mathtt{t_{2}}\rrbracket\llbracket\mathtt{t_{1}}\rrbracket
p=\llbracket\mathtt{t_{1}\cdot t_{2}}\rrbracket p$, while (ii) holds by
induction as ${\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)=\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)=\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(r)=\alpha(q)}$.

(join) : The inductive hypothesis yields
$q_{1}\leq\llbracket\mathtt{t_{1}}\rrbracket p$ and
$q_{2}\leq\llbracket\mathtt{t_{2}}\rrbracket p$, thus by additivity of
$\llbracket\mathtt{\cdot}\rrbracket$,
$q_{1}+q_{2}\leq\llbracket\mathtt{t_{1}}\rrbracket
p+\llbracket\mathtt{t_{2}}\rrbracket
p=\llbracket\mathtt{t_{1}+t_{2}}\rrbracket p$, implying (i). (ii) instead can
be obtained by induction and additivity of $\alpha(\cdot)$:

$\llbracket\mathtt{t_{1}+t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)=\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)+\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q_{1})+\alpha(q_{2})=\alpha(q_{1}+q_{2})$

(rec) : By induction we have that $r\leq\llbracket\mathtt{t}\rrbracket p$. For
any $a\in K$ it holds $a\leq a^{*}$ [18, Section 2.1], and by isotony of
$\boldsymbol{\langle}\cdot\boldsymbol{|}$,

$r\leq\llbracket\mathtt{t}\rrbracket
p=\boldsymbol{\langle}\llbracket\mathtt{t}\rrbracket_{u}\boldsymbol{|}p\leq\boldsymbol{\langle}(\llbracket\mathtt{t}\rrbracket_{u})^{*}\boldsymbol{|}p=\boldsymbol{\langle}\llbracket\mathtt{t^{*}}\rrbracket_{u}\boldsymbol{|}p=\llbracket\mathtt{t^{*}}\rrbracket
p$

Moreover, for any $a\in K$ it holds $a^{*}a^{*}=a^{*}$ [18, Section 2.1], so
that

$\displaystyle\llbracket\mathtt{t^{*}}\rrbracket\llbracket\mathtt{t^{*}}\rrbracket
p$ $\displaystyle=\textrm{[By (\ref{eqn:csema_mul})]}$
$\displaystyle\llbracket\mathtt{t^{*}\cdot t^{*}}\rrbracket p$
$\displaystyle=$
$\displaystyle\boldsymbol{\langle}\llbracket\mathtt{t^{*}\cdot
t^{*}}\rrbracket_{u}\boldsymbol{|}p$ $\displaystyle=$
$\displaystyle\boldsymbol{\langle}(\llbracket\mathtt{t}\rrbracket_{u})^{*}(\llbracket\mathtt{t}\rrbracket_{u})^{*}\boldsymbol{|}p$
$\displaystyle=$ $\displaystyle\llbracket\mathtt{t^{*}}\rrbracket p$

By induction, it holds
$q\leq\llbracket\mathtt{t^{*}}\rrbracket(p+r)=\llbracket\mathtt{t^{*}}\rrbracket
p+\llbracket\mathtt{t^{*}}\rrbracket r$, but
${\llbracket\mathtt{t^{*}}\rrbracket
r\leq\llbracket\mathtt{t^{*}}\rrbracket\llbracket\mathtt{t^{*}}\rrbracket
p=\llbracket\mathtt{t^{*}}\rrbracket p}$, thus implying (i). (ii) can be
retrieved by (i), isotony of
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}$, $\alpha(\cdot)$ and
soundness

$\alpha(q)\leq\alpha(\llbracket\mathtt{t^{*}}\rrbracket
p)\leq\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(p)\leq\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(p+r)=\alpha(q)$

(iterate) : For any $a\in K$ it holds $1\leq a^{*}$ and $a\leq a^{*}$ [18,
Section 2.1], thus by isotony of $\boldsymbol{\langle}\cdot\boldsymbol{|}$,
$q\leq\llbracket\mathtt{t}\rrbracket
p=\boldsymbol{\langle}\llbracket\mathtt{t}\rrbracket_{u}\boldsymbol{|}p\leq\boldsymbol{\langle}(\llbracket\mathtt{t}\rrbracket_{u})^{*}\boldsymbol{|}p=\boldsymbol{\langle}\llbracket\mathtt{t^{*}}\rrbracket_{u}\boldsymbol{|}p\leq\llbracket\mathtt{t^{*}}\rrbracket
p$ and by (5) and isotony of $\boldsymbol{\langle}\cdot\boldsymbol{|}$,
$p=p\cdot
1=\boldsymbol{\langle}1\boldsymbol{|}p\leq\boldsymbol{\langle}(\llbracket\mathtt{t}\rrbracket_{u})^{*}\boldsymbol{|}p=\llbracket\mathtt{t^{*}}\rrbracket
p$, thus implying (i) $p+q\leq\llbracket\mathtt{t^{*}}\rrbracket p$. To show
(ii) we need the following preliminary fact:

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

First, let us prove by induction on $n$ that $\alpha(p)$ 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(p)\leq\alpha(p)$.
The base case $n=0$ is true since
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{0}\alpha(p)=\alpha(p)\leq\alpha(p)$,
while the inductive case holds by isotony of
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}$,
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n+1}\alpha(p)=(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)\leq(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(p)\leq\alpha(p)$.
Notice that $\alpha(p)$ is also the least upper bound because
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{0}\alpha(p)=\alpha(p)$. The
hypothesis $q\leq A(p)$ implies $\alpha(q)\leq\alpha(p)$ by isotony of
$\alpha(\cdot)$ and $\gamma(\cdot)$, (21) and (23). Notice that
${\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q)\leq\alpha(p)}$,
meaning that we can apply (26):

$\displaystyle\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(p)=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(p)=\alpha(p)=\alpha(p)+\alpha(q)=\alpha(p+q).$
∎

Analogously to what happens for $\operatorname{LCL}$, we can prove that
$\operatorname{LCK}_{A}$ is logically complete under these two additional
hypotheses:

  1. (A)

The following infinitary rule is added to $\operatorname{LCK}_{A}$:

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

Let us point out that the lub $\bigvee_{n\in\mathbb{N}}p_{n}$ always exists in
$K$, as a consequence of the CTC requirement on $K$.

  2. (B)

The concrete semantics of the primitive actions and tests occurring in the
program are globally complete.

It can be proved that the rule (limit) preserves logical soundness:

######  Lemma 3 ()

With the hypothesis of Theorem 3.4, the rule (limit) preserves logical
soundness.

###### Proof

Let’s assume that (limit) proves a triple
$[p_{0}]\;\mathtt{t^{*}}\;[\bigvee_{n\in\mathbb{N}}p_{n}]$. The conditions (i)
is $\bigvee_{n\in\mathbb{N}}p_{n}\leq\llbracket\mathtt{t^{*}}\rrbracket
p_{0}$, which is equivalent to $\forall
n\in\mathbb{N}.\;p_{n}\leq\llbracket\mathtt{t^{*}}\rrbracket p_{0}$. The
latter can be shown by induction on $n$. By (17), ${p_{0}\leq
p_{0}+\llbracket\mathtt{t}\rrbracket\llbracket\mathtt{t^{*}}\rrbracket
p_{0}\leq\llbracket\mathtt{t^{*}}\rrbracket p_{0}}$. Similarly for the
inductive case $p_{n+1}\leq\llbracket\mathtt{t}\rrbracket
p_{n}\leq\llbracket\mathtt{t}\rrbracket\llbracket\mathtt{t^{*}}\rrbracket
p_{0}\leq
p_{0}+\llbracket\mathtt{t}\rrbracket\llbracket\mathtt{t^{*}}\rrbracket
p_{0}\leq\llbracket\mathtt{t^{*}}\rrbracket p_{0}$, where the first inequality
holds by structural induction, i.e.,
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p_{n}]\;\mathtt{t}\;[p_{n+1}]$
implies
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p_{n}]\;\mathtt{t}\;[p_{n+1}]$.
To show (ii) we need the auxiliary claim $\forall
n\in\mathbb{N}.\;(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(p_{0})=\alpha(p_{n})$.
That can be proved by induction on $n$. The base case is trivially true as
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{0}\alpha(p_{0})=\alpha(p_{0})$.
While the inductive case holds by structural induction, i.e.,
$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p_{n})=\alpha(p_{n+1})$, as
$(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n+1}\alpha(p_{0})=\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(p_{0})=\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p_{n})=\alpha(p_{n+1})$.
Therefore by additivity of $\alpha(\cdot)$,

$\displaystyle\llbracket\mathtt{t^{*}}\rrbracket_{A}^{\sharp}\alpha(p_{0})=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t}\rrbracket_{A}^{\sharp})^{n}\alpha(p_{0})=\bigvee_{n\in\mathbb{N}}\alpha(p_{n})=\alpha(\bigvee_{n\in\mathbb{N}}p_{n}).$
∎

The condition (B) entails global completeness:

######  Lemma 4 ()

Let $K$ a backward-diamond CTC Kleene algebra, $A$ a Kleene abstract domain on
$K$ and $T_{\Sigma,B}$ a KAT language on $K$. For any $\mathtt{t}\in
T_{\Sigma,B}$ and $p\in\operatorname{\mathsf{test}}(K)$ we have

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

###### Proof

The proof is on the structure of $\mathtt{t}$:

($\mathtt{a}\in\operatorname{Atom}$) :

$\displaystyle\llbracket\mathtt{a}\rrbracket_{A}^{\sharp}\comp\alpha$
$\displaystyle=$
$\displaystyle\alpha\comp\llbracket\mathtt{a}\rrbracket\comp\gamma\comp\alpha$
$\displaystyle=\textrm{[By $\mathbb{C}^{A}(\llbracket\mathtt{a}\rrbracket)$,
(\ref{eqn:gamma_inject})]}$
$\displaystyle\alpha\comp\llbracket\mathtt{a}\rrbracket$

($\mathtt{t_{1}+t_{2}}$) : Let us denote with $p$ a generic test.

$\displaystyle\llbracket\mathtt{t_{1}+t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)$
$\displaystyle=$
$\displaystyle\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)+\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)$
$\displaystyle=\textrm{[By induction]}$
$\displaystyle\alpha(\llbracket\mathtt{t_{1}}\rrbracket
p)+\alpha(\llbracket\mathtt{t_{2}}\rrbracket p)$ $\displaystyle=\textrm{[By
additivity of $\alpha(\cdot)$,$\llbracket\mathtt{\cdot}\rrbracket$]}$
$\displaystyle\alpha(\llbracket\mathtt{t_{1}+t_{2}}\rrbracket p)$

($\mathtt{t_{1}\cdot t_{2}}$) : Let us denote with $p$ a generic test.

$\displaystyle\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket_{A}^{\sharp}\alpha(p)$ $\displaystyle=$
$\displaystyle\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)$
$\displaystyle=\textrm{[By induction]}$
$\displaystyle\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(\llbracket\mathtt{t_{1}}\rrbracket
p)$ $\displaystyle=\textrm{[By induction]}$
$\displaystyle\alpha(\llbracket\mathtt{t_{2}}\rrbracket\llbracket\mathtt{t_{1}}\rrbracket
p)$ $\displaystyle=\textrm{[By (\ref{eqn:csema_mul})]}$
$\displaystyle\alpha(\llbracket\mathtt{t_{1}\cdot t_{2}}\rrbracket p)$

($\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(p)=\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)$
(27)

that can be proved by induction on $n$. The base case is
${(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{0}\alpha(p)=\alpha(p)=\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{0}p)}$.
While the inductive case can be proved as follows

$(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n+1}\alpha(p)=\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(p)=\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)=\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n+1}p)$

Therefore,

$\displaystyle\llbracket\mathtt{t_{0}^{*}}\rrbracket_{A}^{\sharp}\alpha(p)$
$\displaystyle=$
$\displaystyle\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp})^{n}\alpha(p)$
$\displaystyle=\textrm{[By (\ref{eqn:claim_3})]}$
$\displaystyle\bigvee_{n\in\mathbb{N}}\alpha((\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)$
$\displaystyle=\textrm{[By additivity of $\alpha(\cdot)$]}$
$\displaystyle\alpha(\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket)^{n}p)$
$\displaystyle=\textrm{[By (\ref{eqn:csema_star})]}$
$\displaystyle\alpha(\llbracket\mathtt{t_{0}^{*}}\rrbracket p)$ ∎

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

Assume that conditions (A) and (B) hold. If
$\>\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]\>$ then
$\>\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$.

###### Proof

The proof is organized in two parts. In the first part we prove that
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[\llbracket\mathtt{t}\rrbracket
p]$. In the second one instead we prove

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[\llbracket\mathtt{t}\rrbracket
p]$ $\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$

1) The proof is by induction on the structure of $\mathtt{t}\in T_{\Sigma,B}$:

($\mathtt{a}\in\operatorname{Atom}$) : By the global completeness hypothesis
we have $\mathbb{C}^{A}_{p}(\llbracket\mathtt{a}\rrbracket)$, hence (transfer)
yields
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{a}\;[\llbracket\mathtt{a}\rrbracket
p]$.

($\mathtt{t_{1}+t_{2}}$) : Let $q_{i}=\llbracket\mathtt{t_{i}}\rrbracket p$,
and by Lemma 4
$\llbracket\mathtt{t_{i}}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(q_{i})$,
which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{i}}\;[q_{i}]$,
thus by induction
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{i}}\;[q_{i}]$.
Notice that by additivity of $\llbracket\mathtt{\cdot}\rrbracket$,
$q_{1}+q_{2}=\llbracket\mathtt{t_{1}}\rrbracket
p+\llbracket\mathtt{t_{2}}\rrbracket
p=\llbracket\mathtt{t_{1}+t_{2}}\rrbracket p$. Finally, (join) yields the
result
${\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}+t_{2}}\;[\llbracket\mathtt{t_{1}+t_{2}}\rrbracket
p]}$

($\mathtt{t_{1}\cdot t_{2}}$) : Let $q_{1}=\llbracket\mathtt{t_{1}}\rrbracket
p$ and $q_{2}=\llbracket\mathtt{t_{2}}\rrbracket q_{1}$. By Lemma 4
$\llbracket\mathtt{t_{1}}\rrbracket_{A}^{\sharp}\alpha(p)=\alpha(\llbracket\mathtt{t_{1}}\rrbracket
p)$ and
$\llbracket\mathtt{t_{2}}\rrbracket_{A}^{\sharp}\alpha(q_{1})=\alpha(\llbracket\mathtt{t_{2}}\rrbracket
q_{1})$, which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}}\;[q_{1}]$ and
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[q_{1}]\;\mathtt{t_{2}}\;[q_{2}]$,
and by induction
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}}\;[q_{1}]$ and
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[q_{1}]\;\mathtt{t_{2}}\;[q_{2}]$.
Finally, (seq) yields the result
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;[\llbracket\mathtt{t_{1}\cdot t_{2}}\rrbracket p]$, where by (15)
$q_{2}=\llbracket\mathtt{t_{2}}\rrbracket\llbracket\mathtt{t_{1}}\rrbracket
p=\llbracket\mathtt{t_{1}\cdot t_{2}}\rrbracket p$.

($\mathtt{t_{0}^{*}}$) : Let
$p_{n}=(\llbracket\mathtt{t_{0}}\rrbracket)^{n}p$. As preliminary step let us
prove that
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p_{n}]\;\mathtt{t_{0}}\;[p_{n+1}]$
for any $n$. (i) holds because $p_{n+1}=\llbracket\mathtt{t_{0}}\rrbracket
p_{n}$, while (ii) is immediate by Lemma 4,
$\llbracket\mathtt{t_{0}}\rrbracket_{A}^{\sharp}\alpha(p_{n})=\alpha(\llbracket\mathtt{t_{0}}\rrbracket
p_{n})=\alpha(p_{n+1})$. By induction we have $\forall
n\in\mathbb{N}.\;\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p_{n}]\;\mathtt{t_{0}}\;[p_{n+1}]$,
thus (limit) yields the result
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{0}^{*}}\;[\llbracket\mathtt{t_{0}^{*}}\rrbracket
p]$ (notice that $p=(\llbracket\mathtt{t_{0}}\rrbracket)^{0}p=p_{0}$ and by
(16) $\llbracket\mathtt{t_{0}^{*}}\rrbracket
p=\bigvee_{n\in\mathbb{N}}(\llbracket\mathtt{t_{0}}\rrbracket)^{n}p=\bigvee_{n\in\mathbb{N}}p_{n}$).

2) By hypothesis
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$, thus
$q\leq\llbracket\mathtt{t}\rrbracket p$ and also
$A(q)=A(\llbracket\mathtt{t}\rrbracket p)$ so that we can use (relax) to
obtain the result:
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;[q]$. ∎

Summing up, this shows that the local completeness logic $\operatorname{LCL}$
introduced in [5] can be made _fully algebraic_ by means of a natural
interpretation on modal KATs with a backward diamond operator, still
preserving its logical soundness and completeness, which are proved by using
just the algebraic axioms of this class of KATs. Hence, this shows that there
is no need to leverage particular semantic properties of programs to reason on
their local completeness.

###  3.5 An Example of a Language-Theoretic KAT

To give an example digressing from programs and showing the generality of the
KAT-based approach, we describe a language-theoretic model of Kleene algebra,
early introduced by Kozen and Smith [21, Section 3].

Let $\Sigma=\\{\mathtt{u}\\}$ and $B=\\{\mathtt{b}_{1},\mathtt{b}_{2}\\}$ be,
resp., the sets of primitive actions and tests. An _atom_ is a string
$c_{1}c_{2}$, where $c_{i}\in\\{\mathtt{b}_{i},\overline{\mathtt{b}}_{i}\\}$.
If $c_{i}=\mathtt{b}_{i}$, where $i\in\\{1,2\\}$, then $\mathtt{b}_{i}$
appears positively in the atom $c_{1}c_{2}$, while if
$c_{i}=\mathtt{\overline{b}}_{i}$ it appears negatively. A _guarded string_ is
either a single atom or a string
$\alpha_{0}\mathtt{a}_{1}\alpha_{1}...\mathtt{a}_{n}\alpha_{n}$, where
$\alpha_{i}$ are atoms and $\mathtt{a}_{i}\in\Sigma$. If we are only
interested in the first (last) atom of a guarded string
$\alpha\mathtt{a}_{1}\alpha_{1}...\mathtt{a}_{n}\beta$, we may refer to it
through the syntax $\alpha x$ ($x\beta$). Concatenation of guarded strings is
given by a coalesced product operation $\diamond$, which is partially defined
as follows:

$x\alpha\diamond\beta y\triangleq\begin{cases*}x\alpha y&if $\alpha=\beta$\\\
\textrm{undefined}&otherwise\end{cases*}$

The elements of this KAT $\mathcal{G}$ are sets of guarded strings. Thus, $+$
is set union, the product is defined as pointwise coalesced product:

$A\cdot B\triangleq\\{x\diamond y\mid x\in A,y\in B\\},$

while the Kleene iteration is: $A^{*}\triangleq\bigcup_{n\in\mathbb{N}}A^{n}$.
The product identity corresponds to the whole set of atoms
$1_{\mathcal{G}}\triangleq\\{\mathtt{b}_{1}\mathtt{b}_{2},\mathtt{b}_{1}\overline{\mathtt{b}}_{2},\overline{\mathtt{b}}_{1}\mathtt{b}_{2},\overline{\mathtt{b}}_{1}\overline{\mathtt{b}}_{2}\\}$,
while $0_{\mathcal{G}}$ is the empty set. The set of tests is
$\operatorname{\mathsf{test}}(\mathcal{G})\triangleq\wp(1_{\mathcal{G}})$.

It turns out that $\mathcal{G}$ is a bdKAT, whose backward diamond is as
follows: for all $a\in{\mathcal{G}}$ and
$p\in\operatorname{\mathsf{test}}({\mathcal{G}})$,

$\boldsymbol{\langle}a\boldsymbol{|}p=\\{\beta\mid x\beta\in pa\\}.$ (28)

###### Proof

Let $r=\\{\beta\mid x\beta\in pa\\}$. By Lemma 1, it is enough to show that
$r$ is the least $q\in\operatorname{\mathsf{test}}(\mathcal{G})$ satisfying
$pa=paq$.

Let $x\beta\in pa$. By definition, $\beta\in r$ means that
$x\beta\diamond\beta=x\beta$ is contained in $par$. This therefore means that
$pa\leq par$. The opposite inequality is trivial since $r$ is a test, hence
$r\leq 1_{\mathcal{G}}$, and by monotonicity of $\cdot$, we have that $pa\geq
par$, thus implying $pa=par$.

Assume now, by contradiction, that there exists
$t\in\operatorname{\mathsf{test}}(\mathcal{G})$ such that $pa=pat$, $t\leq r$
and $t\neq r$. This means that there is at least an atom $\beta$ in $r$ which
is not in $t$. By definition of $r$, there is a guarded string $x\beta\in pa$.
Since $pa=pat$, the last atom of all the guarded strings in $pa$ must be in
$t$, but this does not hold for $x\beta$ as $\beta\notin t$. ∎

Let us consider the evaluation function
$G:\operatorname{Atom}\rightarrow\mathcal{G}$ as defined in [21]:

$\displaystyle G(\mathtt{a})$
$\displaystyle\triangleq\\{\alpha\mathtt{a}\beta\mid\alpha,\beta\in
1_{\mathcal{G}}\\},$ $\displaystyle G(\mathtt{b})$
$\displaystyle\triangleq\\{\alpha\in 1_{\mathcal{G}}\mid\mathtt{b}\textrm{
appears positively in }\alpha\\}.$

We consider the abstract domain $A\triangleq\\{\top,e,o,\bot\\}$ determined by
the following abstraction
$\alpha:\operatorname{\mathsf{test}}({\mathcal{G}})\rightarrow A$ and
concretization
$\gamma:A\rightarrow\operatorname{\mathsf{test}}({\mathcal{G}})$ maps:

$\displaystyle\alpha(p)\triangleq\begin{cases*}\bot&if $p=\emptyset$\\\ e&if
$\emptyset\subsetneq
p\subseteq\\{\mathtt{b}_{1}\mathtt{b}_{2},\overline{\mathtt{b}}_{1}\overline{\mathtt{b}}_{2}\\}$\\\
o&if $\emptyset\subsetneq
p\subseteq\\{\overline{\mathtt{b}}_{1}\mathtt{b}_{2},\mathtt{b}_{1}\overline{\mathtt{b}}_{2}\\}$\\\
\top&otherwise\end{cases*}$
$\displaystyle\gamma(p^{\sharp})\triangleq\begin{cases*}\emptyset&if
$p^{\sharp}=\bot$\\\
\\{\mathtt{b}_{1}\mathtt{b}_{2},\overline{\mathtt{b}}_{1}\overline{\mathtt{b}}_{2}\\}&if
$p^{\sharp}=e$\\\
\\{\overline{\mathtt{b}}_{1}\mathtt{b}_{2},\mathtt{b}_{1}\overline{\mathtt{b}}_{2}\\}&if
$p^{\sharp}=o$\\\ 1_{\mathcal{G}}&if $p^{\sharp}=\top$\end{cases*}$

By counting, in an atom, the number of primitive tests that appear positively
we obtain an integer that may be even or odd. Hence, this abstract domain $A$
represents the property of being even $e$ or odd $o$ of all the atoms
occurring in a test $p\in\operatorname{\mathsf{test}}({\mathcal{G}})$.

By using our logic $\operatorname{LCK}$, we study the correctness of the
program $\mathtt{r}\triangleq\mathtt{(u\cdot b_{1})^{*}}\in{\mathcal{G}}$,
assuming a precondition
$p\triangleq\\{\mathtt{b}_{1}\mathtt{b}_{2},\overline{\mathtt{b}}_{1}\overline{\mathtt{b}}_{2}\\}\in\operatorname{\mathsf{test}}({\mathcal{G}})$
and a specification $\operatorname{Spec}\triangleq p=\gamma(e)$. Let us define
two auxiliary tests:
$q\triangleq\\{\mathtt{b}_{1}\mathtt{b}_{2},\mathtt{b}_{1}\overline{\mathtt{b}}_{2}\\}$,
$s\triangleq\\{\mathtt{b}_{1}\mathtt{b}_{2},\mathtt{b}_{1}\overline{\mathtt{b}}_{2},\overline{\mathtt{b}}_{1}\overline{\mathtt{b}}_{2}\\}$.
Using the equation (28), we can easily check the following local completeness
equations:

$\displaystyle\alpha(\llbracket\mathtt{u}\rrbracket
A(s))=\alpha(\llbracket\mathtt{u}\rrbracket
1_{\mathcal{G}})=\alpha(1_{\mathcal{G}})=\top=\alpha(1_{\mathcal{G}})=\alpha(\llbracket\mathtt{u}\rrbracket
s)$
$\displaystyle\Rightarrow\;\mathbb{C}^{A}_{s}(\llbracket\mathtt{u}\rrbracket)$
$\displaystyle\alpha(\llbracket\mathtt{u}\rrbracket
A(p))=\alpha(\llbracket\mathtt{u}\rrbracket
p)=\alpha(1_{\mathcal{G}})=\top=\alpha(1_{\mathcal{G}})=\alpha(\llbracket\mathtt{u}\rrbracket
p)$
$\displaystyle\Rightarrow\;\mathbb{C}^{A}_{p}(\llbracket\mathtt{u}\rrbracket)$
$\displaystyle\alpha(\llbracket\mathtt{b_{\text{$1$}}}\rrbracket
A(1_{\mathcal{G}}))=\alpha(\llbracket\mathtt{b_{\text{$1$}}}\rrbracket
1_{\mathcal{G}})=\alpha(q)=\top=\alpha(q)=\alpha(\llbracket\mathtt{b_{\text{$1$}}}\rrbracket
1_{\mathcal{G}})$
$\displaystyle\Rightarrow\;\mathbb{C}^{A}_{1_{\mathcal{G}}}(\llbracket\mathtt{b_{\text{$1$}}}\rrbracket)$

Therefore, we have the following derivation in $\operatorname{LCK}_{A}$ of the
triple $[p]\;\mathtt{r}\;[s]$:

$\mathbb{C}^{A}_{p}(\llbracket\mathtt{u}\rrbracket)$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{u}\;[1_{\mathcal{G}}]$
$\mathbb{C}^{A}_{1_{\mathcal{G}}}(\llbracket\mathtt{b_{\text{$1$}}}\rrbracket)$
(transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[1_{\mathcal{G}}]\;\mathtt{b_{\text{$1$}}}\;[q]$
(seq) $\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{u\cdot
b_{\text{$1$}}}\;[q]$ $\mathbb{C}^{A}_{s}(\llbracket\mathtt{u}\rrbracket)$
(transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[s]\;\mathtt{u}\;[1_{\mathcal{G}}]$
$\mathbb{C}^{A}_{1_{\mathcal{G}}}(\llbracket\mathtt{b_{\text{$1$}}}\rrbracket)$
(transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[1_{\mathcal{G}}]\;\mathtt{b_{\text{$1$}}}\;[q]$
(seq) $\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[s]\;\mathtt{u\cdot
b_{\text{$1$}}}\;[q]$ $\\!\\!\\!\\!\\!\\!\\!\\!\\!q\leq A(s)$ (iterate)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[s]\;\mathtt{(u\cdot
b_{\text{$1$}})^{*}}\;[s]$ (rec)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{(u\cdot
b_{\text{$1$}})^{*}}\;[s]$

Here, in accordance with the soundness Theorem 3.4, we have that
$s\subseteq\llbracket\mathtt{\mathtt{r}}\rrbracket p\subseteq A(s)$. Observe
that $A(s)\nsubseteq\operatorname{Spec}$ holds, meaning that an abstract
interpretation-based analysis fails to prove that the program $\mathtt{r}$ is
correct for $\operatorname{Spec}$. However, unlike conventional abstract
interpretation, $\operatorname{LCK}_{A}$ is capable to show that
$s\smallsetminus\operatorname{Spec}=\\{\mathtt{b}_{1}\overline{\mathtt{b}}_{2}\\}$
is indeed a true alert, meaning that the program $\mathtt{r}$ is really
incorrect and the failure to prove its correctness was not due to a false
alarm.

###  3.6 Under-Approximation Logic

$\mathtt{a}\in\operatorname{Atom}$ (transfer)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{a}\;[\llbracket\mathtt{a}\rrbracket
p]$

$\vdash_{\operatorname{UL}}[p^{\prime}]\;\mathtt{t}\;[q^{\prime}]$ (empty)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t}\;[0]$

$p^{\prime}\leq
p\qquad\vdash_{\operatorname{UL}}[p^{\prime}]\;\mathtt{t}\;[q^{\prime}]\qquad
q\leq q^{\prime}$ (consequence)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]$

$\vdash_{\operatorname{UL}}[p_{1}]\;\mathtt{t}\;[q_{1}]$
$\vdash_{\operatorname{UL}}[p_{2}]\;\mathtt{t}\;[q_{2}]$ (disj)
$\vdash_{\operatorname{UL}}[p_{1}+p_{2}]\;\mathtt{t}\;[q_{1}+q_{2}]$

$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{\text{$1$}}}\;[r]$
$\vdash_{\operatorname{UL}}[r]\;\mathtt{t_{\text{$2$}}}\;[q]$ (seq)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\;[q]$

$\vdash_{\operatorname{UL}}[p^{\prime}]\;\mathtt{t}\;[q^{\prime}]$ (iterate
zero) $\vdash_{\operatorname{UL}}[p]\;\mathtt{t^{*}}\;[p]$

$\vdash_{\operatorname{UL}}[p]\;\mathtt{t^{*}\cdot t}\;[q]$ (iterate non-zero)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t^{*}}\;[q]$

$\forall
n\in\mathbb{N}.\;\vdash_{\operatorname{UL}}[p_{n}]\;\mathtt{t}\;[p_{n+1}]$
(back-v)
$\vdash_{\operatorname{UL}}[p_{0}]\;\mathtt{t^{*}}\;[\bigvee_{n\in\mathbb{N}}p_{n}]$

$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{\text{$i$}}}\;[q]\textrm{, with
$i=1$ or $i=2$}$ (choice)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\;[q]$

Figure 2: Proof System $\operatorname{UL}$.

O’Hearn [26] incorrectness logic ($\operatorname{IL}$) establishes two main
novelties w.r.t. the seminal Hoare logic of program correctness [17]: (1) a
valid postcondition of an incorrectness triple for a program $P$ is an _under-
approximation_ of the strongest postcondition of $P$, rather than an over-
approximation of Hoare logic; (2) incorrectness triples feature two
postconditions: one corresponding to a “normal” program termination and one
corresponding to an erroneous termination. Even if $\operatorname{IL}$ was
originally defined with both those features, we first neglect the second one —
i.e., we consider “normal” termination only — and we refer to the resulting
program logic as Under-approximation Logic, denoted by $\operatorname{UL}$.
For the sake of clarity, Figure 2 recalls the $\operatorname{UL}$ proof
system, adapted to our algebraic framework. We only focus on the
“propositional” fragment of this logic, meaning that the roles of all the
special program commands (i.e., $\mathtt{error}$, $\mathtt{assume}$,
$\mathtt{skip}$, $\mathtt{nondet}$ used in [26]) and variable manipulations
commands of incorrectness logic are played by some corresponding elements in
$\operatorname{Atom}$. Hence, for all of them, the single rule (transfer) is
unifying and enough for our purposes.

Analogously to what has been proved in [5, Section 6] for
$\operatorname{LCL}$, it turns out that the trivial abstraction, i.e., the
abstract domain $A_{tr}\triangleq\\{\top\\}$ that approximates all the
concrete elements to a single abstract element $\top$, allows us to show that
the instantiation $\operatorname{LCK}_{A_{tr}}$, with the additional rule
(limit), boils down to $\operatorname{UL}$, namely, our $\operatorname{LCK}$
logic generalizes $\operatorname{UL}$, even when both are interpreted on KATs.

######  Theorem 3.6 ($\operatorname{LCK}_{A_{tr}}\equiv\operatorname{UL}$)

Let $K$ be a CTC bdKAT. Assume that $\operatorname{LCK}_{A_{tr}}$ includes the
rule (limit). For any $p,q\in\operatorname{\mathsf{test}}(K)$ and
$\mathtt{t}\in T_{\Sigma,B}$:

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]\quad\Leftrightarrow\quad\vdash_{\operatorname{UL}}[p]\;\mathtt{t}\;[q].$

###### Proof

Notice that in the $\operatorname{LCK}_{A_{tr}}$ proof system, the premise
$\mathbb{C}^{A_{tr}}_{p}(\llbracket\mathtt{a}\rrbracket)$ of (transfer) is
always true because $A_{tr}\comp\llbracket\mathtt{a}\rrbracket
p=1=A_{tr}\comp\llbracket\mathtt{a}\rrbracket\comp A_{tr}(p)$ and similarly
the conditions $p\leq A_{tr}(p^{\prime})$ and $q^{\prime}\leq
A_{tr}(q^{\prime})$ of (relax) are always true because $A_{tr}(p)=1$ which is
the greatest element of $\operatorname{\mathsf{test}}(K)$.

Moreover, there is a strong correspondence between the two proof systems: in
particular the rules of Table 1 coincide.

$\operatorname{LCK}_{A_{Tr}}$ | $\operatorname{UL}$
---|---
transfer | transfer
relax | consequence
seq | seq
limit | back-v
Table 1: Correspondence between the rules of $\operatorname{LCK}_{A_{tr}}$ and
$\operatorname{UL}$.

$\Rightarrow)$ As preliminary step, notice that derivation trees built by the
proof of Theorem 3.5 do not require the rules (rec) and (iterate), thus by
soundness and completeness we can build a derivation tree of
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]$ which
does not contain such rules.

The proof is by induction on the derivation tree of
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]$. The
rules of Table 1 are immediate. The only rule left to prove is (join). By
induction we have $\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{1}}\;[q_{1}]$ and
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{2}}\;[q_{2}]$ and we need to show
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{1}+t_{2}}\;[q_{1}+q_{2}]$:

$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{1}}\;[q_{1}]$ (choice)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{1}+t_{2}}\;[q_{1}]$
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{2}}\;[q_{2}]$ (choice)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{1}+t_{2}}\;[q_{2}]$ (disj)
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t_{1}+t_{2}}\;[q_{1}+q_{2}]$

$\Leftarrow)$ The proof is by induction on the derivation tree of
$\vdash_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]$. As in the previous case, the
rules of Table 1 are immediate. The rules that are left to prove are
(empty),(choice),(disj),(iterate zero) and (iterate non-zero).

In order to carry out the derivation in those cases we exploit the
completeness of $\operatorname{LCK}$. To do so we only need to verify
condition (i), because (ii) is trivially true:
$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\top=\alpha(q)=\top=\alpha(\llbracket\mathtt{t}\rrbracket
p)$ for any $p,q\in\operatorname{\mathsf{test}}(K)$ and $\mathtt{t}\in
T_{\Sigma,B}$.

(empty) :
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[0]$ is
trivial since $0\leq\llbracket\mathtt{t}\rrbracket p$ is always true,
therefore by completeness of $\operatorname{LCK}_{A_{tr}}$,
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[0]$.

(choice) : By induction we have, without loss of generality,
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}}\;[q]$ and
we need to show
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}+t_{2}}\;[q]$.
Notice that for any $\mathtt{t_{2}}\in T_{\Sigma,B}$,
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{2}}\;[0]$
because (i) is trivially true: $0\leq\llbracket\mathtt{t_{2}}\rrbracket p$,
therefore by completeness of $\operatorname{LCK}_{A_{tr}}$
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{2}}\;[0]$.
Finally, (join) yields the result
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t_{1}+t_{2}}\;[q]$.

(disj) : By induction we have
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p_{1}]\;\mathtt{t}\;[q_{1}]$
and
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p_{2}]\;\mathtt{t}\;[q_{2}]$
and we need to show
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p_{1}+p_{2}]\;\mathtt{t}\;[q_{1}+q_{2}]$.
By soundness we have
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p_{1}]\;\mathtt{t}\;[q_{1}]$
and
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p_{2}]\;\mathtt{t}\;[q_{2}]$,
meaning $q_{1}\leq\llbracket\mathtt{t}\rrbracket p_{1}$ and
$q_{2}\leq\llbracket\mathtt{t}\rrbracket p_{2}$, so that
$q_{1}+q_{2}\leq\llbracket\mathtt{t}\rrbracket(p_{1}+p_{2})$. Finally, by
completeness we retrieve the result:
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p_{1}+p_{2}]\;\mathtt{t}\;[q_{1}+q_{2}]$.

(iterate zero) : By (17) it holds $\llbracket\mathtt{t^{*}}\rrbracket p\geq p$
which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}}\;[p]$,
and by completeness we obtain the result
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}}\;[p]$.

(iterate non-zero) : By (17) it holds $\llbracket\mathtt{t^{*}}\rrbracket
p\geq\llbracket\mathtt{t^{*}\cdot t}\rrbracket p$. By hypothesis
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}\cdot
t}\;[q]$, hence by soundness $q\leq\llbracket\mathtt{t^{*}\cdot t}\rrbracket
p$. Combining the two we yields $q\leq\llbracket\mathtt{t^{*}}\rrbracket p$,
which means
$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}}\;[q]$
and by completeness
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t^{*}}\;[q]$. ∎

Moreover, since the abstraction map defining $A_{tr}$ is
$\alpha_{A_{tr}}=\lambda x.\top$, we have that condition (ii) of Definition
3.3 for the validity of a $\operatorname{LCK}$ triple trivially holds, that
is,
$\llbracket\mathtt{t}\rrbracket_{A}^{\sharp}\alpha(p)=\top=\alpha(q)=\alpha(\llbracket\mathtt{t}\rrbracket^{K}p)$.
This therefore entails that

$\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]\quad\Leftrightarrow\quad\models_{\operatorname{UL}}[p]\;\mathtt{t}\;[q].$
(29)

This allows us to retrieve the soundness and completeness results of
incorrectness logic [26] as a consequence of those for $\operatorname{LCK}$.

######  Corollary 1 ()

Under the same hypotheses of Theorem 3.6, 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:lcl_ul_equiv}]}$
$\displaystyle\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]$
$\displaystyle\Leftrightarrow\qquad\textrm{[by Theorems \ref{thm:lsound} and
\ref{thm:lcompl}]}$
$\displaystyle\models^{{\scriptscriptstyle\mathrm{K}}}_{A_{tr}}[p]\;\mathtt{t}\;[q]$
$\displaystyle\Leftrightarrow\qquad\textrm{[by \eqref{equiv3}]}$
$\displaystyle\models_{\operatorname{UL}}[p]\;\mathtt{t}\;[q]$ ∎

##  4 Incorrectness Logic in KAT

Incorrectness logic $\operatorname{IL}$ has been introduced by O’Hearn [26] as
a natural under-approximating counterpart of the pivotal Hoare correctness
logic [17], and quickly attracted a lot of research interest [29, 28, 22, 33,
27]. Incorrectness logic distinguishes two postconditions corresponding to
normal and erroneous/abnormal program termination. Here, we generalize the
algebraic formulation of our $\operatorname{LCK}$ logic to support abnormal
termination. We follow the approach of Möller, O’Hearn and Hoare [24], namely,
each language term is interpreted as a pair of KAT elements which model the
normal and abnormal execution. The evaluation function has type
$u:\operatorname{Atom}\rightarrow(K\times K)$, while the interpretation
function has type
$\llbracket\mathtt{\cdot}\rrbracket_{u}:T_{\Sigma,B}\rightarrow(K\times K)$.
As a shorthand $\llbracket\mathtt{\cdot}\rrbracket_{u}$ can be subscripted
with  ok or  err to denote, resp., its first normal and second erroneous
component. The definition is as follows:

$\displaystyle\llbracket\mathtt{a}\rrbracket_{u}$ $\displaystyle\triangleq
u(\mathtt{a})$ (30)
$\displaystyle\llbracket\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\rrbracket_{u}$
$\displaystyle\triangleq({\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_{\text{$1$}}}\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]{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_{\text{$2$}}}\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}\llbracket\mathtt{t_{\text{$1$}}}\rrbracket_{u_{\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}\llbracket\mathtt{t_{\text{$2$}}}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})$ $\displaystyle\llbracket\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\rrbracket_{u}$
$\displaystyle\triangleq({\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_{\text{$1$}}}\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
}}}}}\cdot{\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_{\text{$2$}}}\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}\llbracket\mathtt{t_{\text{$1$}}}\rrbracket_{u_{\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_{\text{$1$}}}\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
}}}}}\cdot{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{\text{$2$}}}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}})$ $\displaystyle\llbracket\mathtt{t^{*}}\rrbracket_{u}$
$\displaystyle\triangleq({\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
}}}}^{*}},{\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
}}}}^{*}}\cdot{\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 }}}}})$

Following the original definition of $\operatorname{IL}$, the precondition
encodes an  ok condition only, while the postcondition contains both an  ok
and an  err component. Hence, the latter is given by a pair
$(p,q)\in\operatorname{\mathsf{test}}(K)\times\operatorname{\mathsf{test}}(K)$,
typically denoted by
$\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}:p},\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}:q}$.
The concrete semantics
$\llbracket\mathtt{\cdot}\rrbracket:T_{\Sigma,B}\rightarrow(\operatorname{\mathsf{test}}(K)\rightarrow(\operatorname{\mathsf{test}}(K)\times\operatorname{\mathsf{test}}(K)))$
is defined as

$\llbracket\mathtt{t}\rrbracket
p\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}:\boldsymbol{\langle}{\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
}}}}}\boldsymbol{|}p},\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}:\boldsymbol{\langle}{\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 }}}}}\boldsymbol{|}p}$

To refer to one of its components, $\llbracket\mathtt{\cdot}\rrbracket$ can be
subscripted with  ok or  err , e.g.,
${\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$.

Like for the $\operatorname{LCK}$ formulation, the concrete semantic of
$\operatorname{LCIL}$ leverages the backward-diamond operator, therefore it
inherits its properties (e.g., isotony, additivity). Moreover, by (1), (bd2)
we have that

$\displaystyle{\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$
$\displaystyle={\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$ (31)
$\displaystyle{\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$
$\displaystyle={\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$ (32)

Given a Kleene abstract domain $A$ on $K$, the corresponding abstract
semantics
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}:T_{\Sigma,B}\rightarrow(A\rightarrow(A\times
A))$ is defined as follows:

$\begin{aligned}
\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({\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
}}}}\gamma(p^{\sharp}))},\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({\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 }}}}\gamma(p^{\sharp}))}\\\
\llbracket\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\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}:{\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_{\text{$1$}}}\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
}}}}}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{t_{\text{$2$}}}\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
}}}}}p^{\sharp}},\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}:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{\text{$1$}}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}p^{\sharp}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{\text{$2$}}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}p^{\sharp}}\\\ \llbracket\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\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}:{\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_{\text{$2$}}}\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
}}}}}({\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_{\text{$1$}}}\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
}}}}}p^{\sharp})},\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}:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{\text{$1$}}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}p^{\sharp}+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{\text{$2$}}}\rrbracket^{\sharp}_{A_{\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_{\text{$1$}}}\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 }}}}}p^{\sharp})}\\\
\llbracket\mathtt{t^{*}}\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}:{\textstyle\bigvee_{n\in\mathbb{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{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
}}}}})^{n}p^{\sharp}},\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}:{\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
}}}}}{\textstyle\bigvee_{n\in\mathbb{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{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 }}}}})^{n}p^{\sharp}}\end{aligned}$

(33)

The  ok part coincides with the semantics of $\operatorname{LCK}$, while the
err component puts in place some differences. In particular, the composition
exhibits a short-circuiting behavior, meaning that an error in the first
command aborts the execution without executing the second one, while the
Kleene star allows an error to occur after some error-free iterations. It is
straightforward to check that this definition of abstract semantics is
monotonic and sound.

The proof system $\operatorname{LCK}$ can be extended with incorrectness
triples. In particular, a triple
$[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]}$
is valid if the standard validity conditions hold for both  ok and  err .

######  Definition 4.1 (Incorrectness Triple)

Let $K$ be a CTC bdKAT $K$ and $T_{\Sigma,B}$ be a language interpreted on
$K$. An _incorrectness triple_ is either
$[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]}$
or
$[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$,
where $p,q,r\in\operatorname{\mathsf{test}}(K)$ and $\mathtt{t}\in
T_{\Sigma,B}$.

Let $A$ be a Kleene abstract domain on $K$ with abstraction map
$\alpha:\operatorname{\mathsf{test}}(K)\rightarrow A$.

  * •

The triple
$[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]}$
is valid if: (1)
$q\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}\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 (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(p)=\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)$.

  * •

The triple
$[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
is valid if: (1)
$r\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$, 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(p)=\alpha(r)=\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)$.

  * •

A triple
$[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]}$
is valid when both
$[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]}$
and
$[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
are valid. In particular, if $q=r$ then the triple
$[p]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$
is valid. ∎

The proof system $\operatorname{LCIL}_{A}$ defining the local completeness
incorrectness logic is given in Figure 3.

$\mathtt{a}\in\operatorname{Atom}\qquad\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
}}}})\qquad\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 }}}})$ (transfer)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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]}$

$p^{\prime}\leq p\leq
A(p^{\prime})\qquad\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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}\leq A(q)$ (relax)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q]}$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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^{{\scriptscriptstyle\mathrm{K}}}_{A}[r]\;\mathtt{t_{\text{$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}[\mathbf{ok}:q]}$
(seq-ok)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}\cdot
t_{\text{$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}[\mathbf{ok}:q]}$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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}:q]}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[q]\;\mathtt{t_{\text{$2$}}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:s]}$
(seq-err)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}\cdot
t_{\text{$2$}}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r+s]}$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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^{{\scriptscriptstyle\mathrm{K}}}_{A}[q]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
(rec-err)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t^{*}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$

$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q_{1}]}$
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$2$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q_{2}]}$
(join)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{\text{$1$}}+t_{\text{$2$}}}\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[\boldsymbol{\epsilon}:q_{1}+q_{2}]}$

$\forall
n\in\mathbb{N}.\;\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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}]}$
(limit)
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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}]}$

Figure 3: Proof system $\operatorname{LCIL}_{A}$.

######  Theorem 4.2 (Logical Soundness of $\operatorname{LCIL}_{A}$)

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

###### Proof

Definitions of
${\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{\cdot}\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]{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{\cdot}\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 }}}}}$ coincide, resp., with $\llbracket\mathtt{\cdot}\rrbracket_{u}$ and
$\llbracket\mathtt{\cdot}\rrbracket_{A}^{\sharp}$ of $\operatorname{LCK}$, and
the  ok part of $\operatorname{LCIL}$ is a subset of
$\operatorname{LCK}$111Here, we refer to the proof system $\operatorname{LCK}$
with the additional rule (limit).. For this reason the soundness of the  ok
part of the triple follows by Theorem 3.4. Moreover, the base case
$\mathtt{t}\equiv\mathtt{a}\in\operatorname{Atom}$ and the inductive case
$\mathtt{t}\equiv\mathtt{t_{1}+t_{2}}$ of
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{\cdot}\rrbracket_{u_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}$ and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{\cdot}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}$ are completely symmetric to their  ok counterparts. For this reason
the  err part of (transfer),(join) can be shown in the same way as the  ok
one. Likewise, the soundness of the  err part of (relax) follows as for the
ok one.

The only cases that are left to prove are (seq-err) and (rec-err). As in
Theorem 3.4, notice that the first equality of (2) entails the second one,
i.e., if
${\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)=\alpha(r)$ is true, then
${\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)=\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)$. For this reason it is enough to show only the former.

(seq-err) : By induction we have
$q\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$,
$r\leq{\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$ and
$s\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 }}}}q$, thus
$s\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
}}}}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
}}}}{\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$. By (31) we have that
${\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 r+s$, thus implying (1). By induction we have
${\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^{\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)$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(p)=\alpha(r)$ and
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(q)=\alpha(s)$, so that
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket^{\sharp}_{A_{\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^{\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)={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(q)=\alpha(s)$. By definition of
${{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}}$, we can prove (2) as follows

$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}\cdot
t_{2}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}}}\alpha(p)$ $\displaystyle=$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}\alpha(p)+{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket^{\sharp}_{A_{\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^{\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)$ $\displaystyle=$ $\displaystyle\alpha(r)+\alpha(s)$
$\displaystyle=\textrm{[Additivity of $\alpha(\cdot)$]}$
$\displaystyle\alpha(r+s).$

(rec-err) : By induction we have
$q\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^{*}}\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$,
$r\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 }}}}q$. By (32) we have that
${{\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\geq{\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 }}}}q\geq r}$, thus implying (1). By induction we have 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(p)=\alpha(q)$ 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(q)=\alpha(r)$. Using the definition of
${\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 }}}}}$ we can prove (2) 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)={\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
}}}}}{\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(p)={\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(q)=\alpha(r)$. ∎

Furthermore, it turns out that $\operatorname{LCIL}_{A}$ is logically
complete.

######  Lemma 5 ()

Let $A$ be a Kleene abstract domain on a CTC bdKAT $K$ and $T_{\Sigma,B}$ be a
language interpreted on $K$. If the atoms in $\mathtt{t}\in T_{\Sigma,B}$ are
globally complete, i.e., for all
$\mathtt{a}\in\operatorname{Atom}(\mathtt{t})$,
$\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_{\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_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$, then, for any $p\in\operatorname{\mathsf{test}}(K)$,
${\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(p)=\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_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}\alpha(p)=\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)}$.

###### Proof

Analogous to the proof of Lemma 4. ∎

######  Theorem 4.3 (Logical Completeness of $\operatorname{LCIL}_{A}$)

Let $A$ be a Kleene abstract domain on a CTC bdKAT $K$ and $T_{\Sigma,B}$ be a
language interpreted on $K$. Assume that the atoms in $\mathtt{t}\in
T_{\Sigma,B}$ are globally complete, i.e., for all
$\mathtt{a}\in\operatorname{Atom}(\mathtt{t})$,
$\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_{\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_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err }}}})$ hold. If
$\>[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]}\>$
is valid, then it is provable in $\operatorname{LCIL}_{A}$.

###### Proof

As discussed in the proof of Theorem 4.2, the  ok part of the semantic
coincides with the $\operatorname{LCK}$ logic, so that
$[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]}$
is provable by the completeness theorem of $\operatorname{LCK}_{A}$. For this
reason only
$[p]\;\mathtt{t}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$
must be shown. The proof is by induction on the structure of $\mathtt{t}\in
T_{\Sigma,B}$. By construction, the  err base case
$\mathtt{t}\equiv\mathtt{a}\in\operatorname{Atom}$ and the inductive case
$\mathtt{t}\equiv\mathtt{t_{1}+t_{2}}$ are symmetric to their  ok
counterparts, so that the proof of those cases is equivalent to Theorem 3.5.
Therefore we only need to prove $\cdot$ and ∗.

($\mathtt{t_{1}\cdot t_{2}}$) : Consider the following assignments (the
equality after the $\Rightarrow$ sign is true by Lemma 5):

$\displaystyle
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{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$
$\displaystyle\Rightarrow{\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^{\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({\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)=\alpha(s)$ $\displaystyle
t={\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$
$\displaystyle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{1}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}\alpha(p)=\alpha({\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)=\alpha(t)$ $\displaystyle
u={\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 }}}}s$
$\displaystyle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\llbracket\mathtt{t_{2}}\rrbracket^{\sharp}_{A_{\textbf{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}
err
}}}}}\alpha(s)=\alpha({\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 }}}}s)=\alpha(u)$

and by induction we have that

$\displaystyle\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[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}:s]}$
$\displaystyle\Rightarrow\;\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[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}:s]}$
$\displaystyle\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:t]}$
$\displaystyle\Rightarrow\;\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:t]}$
$\displaystyle\models^{{\scriptscriptstyle\mathrm{K}}}_{A}[s]\;\mathtt{t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:u]}$
$\displaystyle\Rightarrow\;\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[s]\;\mathtt{t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:u]}$

Then by (seq-err) the triple $[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:t+u]}$
is provable. By hypothesis we have

$r\leq{\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\stackrel{{\scriptstyle(\ref{eqn:csema_err_mul})}}{{=}}{\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=t+u$

and

$\alpha(r)=\alpha({\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)=\alpha(t+u)$

so that we can apply (relax) to obtain the result
$\vdash^{{\scriptscriptstyle\mathrm{K}}}_{A}[p]\;\mathtt{t_{1}\cdot
t_{2}}\;{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[\mathbf{err}:r]}$.

($\mathtt{t_{0}^{*}}$) : Let
$q={\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$ and
$s={\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$. By Lemma 5