thesis.tex

\documentclass[
  10pt,       % fontsize
  twoside,    % symmetric pagination, for digital view
  % oneside,  % asymmetric pagination, for a nice printed version
  a4paper,    % 
  english,    % 
  tikz,       % to build images
  openright,  % start chapters on odd-numbered pages
]{book}


\usepackage{preamble}
\usepackage{graphicx}
\graphicspath{ {./images/} }

\begin{document}

%% config && title page
\frontmatter
%!TEX root = ../dissertation.tex

\newcommand{\myName}{Alessio Ferrarini}
\newcommand{\myTitle}{Abstract Hoare logic}
\newcommand{\myDegree}{Master degree thesis}
\newcommand{\myUni}{University of Padova}
\newcommand{\myFaculty}{Master degree in Computer Science}
\newcommand{\myDepartment}{Department of Mathematics ``Tullio Levi-Civita''}
\newcommand{\profTitle}{Prof.}
\newcommand{\myProf}{Francesco Ranzato}
\newcommand{\myCoProf}{Paolo Baldan}
\newcommand{\myLocation}{Padova}
\newcommand{\myAA}{2023--2024}
\newcommand{\myTime}{April}

\title{\myTitle}
\author{\myName}

% PDF file metadata fields
% when updating them delete the build directory, otherwise they won't change
\begin{filecontents*}{\jobname.xmpdata}
  \Title{Abstract Hoare logic}
  \Author{Alessio Ferrarini}
  \Language{en-EN}
  \Subject{Software Verification}
  \Keywords{Hoare Logic\sep Software Verification\sep Abstract Interpretation}
\end{filecontents*}

% IMPORTANT: Update the metadata!! Contains the subject and the
% keywords

% Author in metadata must be specified again, otherwise it won't
% compile

\begin{titlepage}
  \begin{center}

    \begin{figure}[htbp]
      \centering
      \includegraphics[height=3cm]{unipd-logo}
    \end{figure}

    \vbox to0pt{
      \vbox to\textheight{
        \vfill \includegraphics[width=11.5cm]{unipd-light}
        \vfill}
      \vss}

    \begin{huge}
      \textbf{\myUni}\\
    \end{huge}

    \line(1, 0){\textwidth} \\
    
    \begin{Large}
      \textsc{\myDepartment}\\
    \end{Large}
    
    \vspace{10pt}
    
    \begin{large}
      \textsc{\myFaculty}\\
    \end{large}

    \vspace{30pt}

    \begin{LARGE}
      {\color{unipdred}\textbf{\myTitle}}\\
    \end{LARGE}

    %% \vspace{40pt}
    \vfill

    \begin{large}
      \begin{flushleft}
        \textit{Supervisor}\\
        \vspace{5pt}
        \profTitle\ \myProf\\
        \vspace{20pt}
        \textit{Co. Supervisor}\\
        \vspace{5pt}
        \profTitle\ \myCoProf\\
      \end{flushleft}

      % You can tweak the spacing to have professor and student names on the same line
      % useful if the page is broken by a long thesis title and you need more space
      \vspace{-55pt}

      \begin{flushright}
        \textit{Candidate}\\
        \vspace{5pt}
        \myName
      \end{flushright}
    \end{large}

    %% \vspace{40pt}

    \line(1, 0){\textwidth} \\
    \begin{normalsize}
      \textsc{Academic Year \myAA}
    \end{normalsize}
  \end{center}
\end{titlepage}
\cleardoublepage
\phantomsection
\pdfbookmark{Abstract}{Abstract}
\begingroup

\chapter*{Abstract}

In theoretical computer science, program logics are essential for verifying the
correctness of software. Hoare logic provides a systematic way of reasoning
about program correctness using preconditions and postconditions. This thesis
explores the development and application of an abstract Hoare-like logic framework
that generalizes the traditional Hoare program logic by using arbitrary elements of
complete lattices as the assertion language, extrapolating what makes Hoare
logic sound and complete. We also demonstrate the practical applications of
this framework by systematically deriving a program logic for hyperproperties, thus highlighting
versatility and benefits of our general framework. From the design of Abstract Hoare logic, we
then define Reverse Abstract Hoare logic, which is used to develop a proof system for
backward correctness reasoning on programs.

\vfill
\cleardoublepage
\phantomsection
\pdfbookmark{Acknowledgments}{Acknowledgments}

\begingroup

\chapter*{Acknowledgments}

Innanzitutto, vorrei ringraziare i miei relatori, Prof. Francesco Ranzato e
Prof. Paolo Baldan, per la paziente supervisione durante lo sviluppo di questa
tesi e per i preziosissimi consigli. Vorrei ringraziarli anche, assieme alla
Prof.ssa Maria Emilia Maietti e al Prof. Ingo Blechschmidt, per avermi fatto
scoprire quanto sia profonda e bella l'informatica.
\\

Un grazie speciale va a tutti gli amici che hanno reso indimenticabili i miei
cinque anni a Padova. Arrivando in questa città il primo giorno senza conoscere
nessuno, non avrei mai immaginato di trovare qui una seconda casa grazie a voi.
Ogni momento trascorso insieme è stato un capitolo prezioso e divertente della
mia esperienza universitaria. Anche se le nostre strade si separeranno e ci
porteranno in posti diversi, sono certo che l'amicizia che abbiamo formato
durerà per sempre.
\\

Also, I would like to thank all the friends I made during my exchange in
Amsterdam, who made me feel at home in a place where I did not know anyone.
Thank you for all the beautiful experiences we had together. See you around the
world.
\\

Infine, vorrei dedicare un sentito ringraziamento alla mia famiglia, in
particolare ai miei genitori. Il vostro sostegno incondizionato e la vostra
fiducia in me sono stati la spinta costante che mi ha motivato a perseguire i
miei sogni. I sacrifici che avete fatto per farmi studiare e crescere sono
inestimabili, e questa tesi è il risultato tangibile del vostro amore e
supporto. Dedico a voi questa tesi.

\bigskip
Alessio Ferrarini

\begin{textblock}{1}[1,1](8,4)
  \epigraph{\textit{``Progress is possible only if we train ourselves to think 
  about programs without thinking of them as pieces of executable code.``}}
  {Edsger W. Dijkstra}
\end{textblock}


\endgroup
\cleardoublepage

%% TOC
\cleardoublepage

\begingroup
\hypersetup{linkcolor=black}
\tableofcontents
\endgroup

%% Structure
\cleardoublepage
\mainmatter
% This file only puropouse is to organize the chapters

% import the mod file from each directory, it will tell how the
% chapter is organized
\chapter*{Introduction}

The verification of program correctness is a critical and crucial task in
computer science. Ensuring that software behaves as expected under all possible
conditions is fundamental in a society that increasingly relies on computer
programs. Software engineers often reason about the behavior of their programs
at an intuitive level. While this is definitely better than not reasoning at
all, intuition alone becomes insufficient as the size of programs grows.

Writing tests for programs is definitely a useful task, but at best, it can
show the presence of bugs, not prove their absence. We cannot feasibly write
tests for every possible input of the program. To offer a guarantee of the
absence of undesired behaviors, we need sound logical models rooted in logic.
The field of formal methods in computer science aims at developing the logical
tools necessary to prove properties of software systems.

Hoare logic, first introduced by Hoare in the late 60s \cite{Hoare69}, provides
a set of logical rules to reason about the correctness of computer programs.
Hoare logic formalizes, with axioms and inference rules, the relationship
between the initial and final states after executing a program.

Hoare logic, beyond being one of the first program logics, is arguably also one
of the most influential ideas in the field of software verification. It created
the whole field of program logics—systems of logical rules aimed at proving
properties of programs. Over the years, modifications of Hoare logic have been
developed, sometimes to support new language features such as dynamic memory
allocation and pointers, or to prove different properties such as equivalence
between programs or properties of multiple executions. Every time Hoare logic
is modified, it is necessary to prove again that the proof system indeed proves
properties about the program (soundness) and ideally that the proof system is
powerful enough to prove all the properties of interest (completeness).

Most modifications of Hoare logic usually do not alter the fundamental proof
principles of the system. Instead, they often extend the assertion language to
express new properties and add new commands to support new features in
different programming languages.

In this work, we introduce Abstract Hoare Logic, which aims to be a framework
general enough to serve as an extensible platform for constructing new
Hoare-like logics without the burden of proving soundness and completeness
anew. We demonstrate, through examples, how some properties that are not
expressible in standard Hoare logic can be simply instantiated within Abstract
Hoare Logic, while keeping the proof system as simple as possible.

The theory of Abstract Hoare Logic is deeply connected to the theory of
abstract interpretation \cite{Cousot77}. The semantics of the language is
defined as an inductive abstract interpreter, and the validity of the Abstract
Hoare triples depends on it. Since we do not use the strongest postcondition
directly, we are able to reason about properties that are not expressible in
the powerset of the program states, such as hyperproperties.

This thesis is structured as follows:
\begin{itemize}
  \item In Chapter 1, we introduce the basic mathematical background of order
    theory and abstract interpretation.

  \item In Chapter 2, we introduce standard Hoare logic and the general
    framework of Abstract Hoare Logic: the extensible language $\lang$, its
    syntax and semantics, the generalization of the strongest postcondition,
    and finally, Abstract Hoare Logic and its proof system, proving the general
    results of soundness and relative completeness.

  \item In Chapter 3, we show some notable instantiations of Abstract Hoare
    Logic: we demonstrate that it is possible to obtain program logics where
    the implication is decidable, thus making the goal of checking a derivation
    computable; we show how to obtain a proof system for hyperproperties (and
    we introduce the concept of the strongest hyper postcondition); finally, we
    show that it is possible to obtain a proof system for partial
    incorrectness.

  \item In Chapter 4, we show how to enrich the barebones proof system of
    Abstract Hoare Logic by adding more restrictions on the assertion language
    or the semantics.

  \item In Chapter 5, we show how to reuse the idea of Abstract Hoare Logic to
    generalize proof systems for backward reasoning.

  \item In Chapter 6, we provide a brief summary of the most important
    contributions of the thesis. We discuss possible extensions to the
    framework of Abstract Hoare Logic and, to conclude, we examine the
    relationship of Abstract Hoare Logic with other similar work.
\end{itemize}

\chapter{Background}

\section{Order theory}\label{sec:backround:order_theory}

When defining the semantics of programming languages, the theory of 
\textit{partially ordered sets} and \textit{lattices} is fundamental
\cite{Gratzer11, Birkhoff40}. These 
concepts are at the core of denotational semantics \cite{Scott70} and 
\textit{Abstract Interpretation} \cite{Cousot77}, where the semantics of 
programming languages and abstract interpreters are defined as monotone 
functions over some complete lattice.

\subsection{Partial Orders}

\begin{definition}[Partial order]
  A partial order on a set $X$ is a relation $\leq \subseteq X \times X$ 
  such that the following properties hold:
  \begin{itemize}
    \item Reflexivity: $\forall x \in X, \; (x, x) \in \; \leq$
    \item Anti-symmetry: $\forall x, y \in X, \; (x, y) \in \; \leq \mand
      (y, x) \in \; \leq \implies x = y$
    \item Transitivity: $\forall x, y, z \in X, \; (x, y) \in \; \leq \mand 
      (y, z) \in \; \leq \implies (x, z) \in \;\leq$
  \end{itemize}
    
\end{definition}

Given a partial order $\leq$, we will use $\geq$ to denote the converse 
relation $\{ (y, x) \mid (x, y) \in \;\leq \}$ and $<$ to denote 
$\{ (x, y) \mid (x, y) \in \;\leq \; \text{and} \; x \neq y \}$.

From now on we will use the notation $x R y$ to indicate $(x, y) \in R$.

\begin{definition}[Partially ordered set]
  A partially ordered set (or poset) is a pair $(X, \leq)$ in which $\leq$ is a 
  partial order on $X$.
\end{definition}

We will use partially ordered sets to encode collections of program states.

\begin{definition}[Galois connection]
  Let $(C, \sqsubseteq)$ and $(A, \leq)$ be two partially ordered sets, a 
  Galois connection written $\langle C, \sqsubseteq \rangle 
  \galois{\alpha}{\gamma} \langle A, \leq \rangle$, are a pair of functions:
  $\gamma : A \to D$ and $\alpha : D \to A$ such that:
  \begin{itemize}
    \item $\gamma$ is monotone
    \item $\alpha$ is monotone
    \item $\forall c \in C$ $c \sqsubseteq \gamma(\alpha(c))$
    \item $\forall a \in A$ $a \leq \alpha(\gamma(a))$
  \end{itemize}
\end{definition}

In the context of program analysis, it is common to refer to $C$ as the concrete
domain and to $A$ as the abstract domain, as the idea behind the use of Galois
connections is to relate $C$ to a simpler and approximate representation of
itself.

\begin{definition}[Galois Insertion]
  Let $\langle C, \sqsubseteq \rangle \galois{\alpha}{\gamma} \langle A, \leq 
  \rangle$, be a Galois connection, a Galois insertion written 
  $\langle C, \sqsubseteq \rangle \galoiS{\alpha}{\gamma} \langle A, \leq \rangle$
  are a pair of functions: $\gamma : A \to D$ and $\alpha : D \to A$ such that:
  \begin{itemize}
    \item $(\gamma, \alpha)$ are a Galois connection
    \item $\alpha \circ \gamma = id$
  \end{itemize}
\end{definition}

Galois insertions are a refinement of Galois connections. By requiring $\alpha
\circ \gamma = id$, we are ensuring that all the abstract elements $a \in A$
have distinct concrete representations. It is always possible to obtain a
Galois insertion from a Galois connection by simply removing all the elements
$a$ such that $\alpha(\gamma(a)) \neq a$ from $A$.

\subsection{Lattices}

\begin{definition}[Meet-semilattice]
  A meet-semilattice is a partially ordered set \((L, \leq)\) such that for
  every pair of elements \(a, b \in L\), there exists an element \(c \in L\)
  satisfying the following conditions: 
  \begin{enumerate}
    \item \(c \leq a\) and \(c \leq b\) 
    \item \(\forall d \in L\), if \(d \leq a\) and \(d \leq b\), then \(d \leq c\) 
\end{enumerate}
  The element \(c\) is called the \emph{meet} of \emph{greatest lower bound} of
  \(a\) and \(b\), and is denoted by \(a \wedge b\).
\end{definition}

\begin{definition}[Join-semilattice]
  A join-semilattice is a partially ordered set \((L, \leq)\) such that for
  every pair of elements \(a, b \in L\), there exists an element \(c \in L\)
  satisfying the following conditions: 
  \begin{enumerate}
    \item \(c \geq a\) and \(c \geq b\) 
    \item \(\forall d \in L\), if \(d \geq a\) and \(d \geq b\), then \(d \geq c\) 
\end{enumerate}
  The element \(c\) is called the \emph{join} or \emph{least upper bound} of
  \(a\) and \(b\), and is denoted by \(a \join b\).
\end{definition}

\begin{observation}
  Both join and meet operations are idempotent, associative, and commutative.
\end{observation}

\begin{definition}[Lattice]
  A poset $(L, \leq)$ is a lattice if it is both a join-semilattice and a 
  meet-semilattice.
\end{definition}

\begin{definition}[Complete lattice]
  A partially ordered set \((L, \leq)\) is called a \emph{complete lattice} if
  for every subset \(S \subseteq L\), there exist elements \(\sup S\) and
  \(\inf S\) in \(L\) such that: 
  \begin{enumerate}
    \item \(\sup S\) (the supremum or least upper bound of \(S\)) is an
      element of \(L\) satisfying: 
      \begin{itemize}
        \item For all \(s \in S\), \(s \leq \sup S\).
        \item For any \(u \in L\), if \(s \leq u\) for all \(s \in S\), then
          \(\sup S \leq u\). \end{itemize}
    \item \(\inf S\) (the infimum or greatest lower bound of \(S\)) is an
      element of \(L\) satisfying: 
      \begin{itemize}
        \item For all \(s \in S\), \(\inf S \leq s\).
        \item For any \(l \in L\), if \(l \leq s\) for all \(s \in S\), then
          \(l \leq \inf S\). 
      \end{itemize}
  \end{enumerate}

  We denote the \textit{least element} or \textit{bottom} as $\bot = \inf \; L$ 
  and the \textit{greatest element} or \textit{top} as $\top = \sup \; L$.
\end{definition}

\begin{observation}
  A complete lattice cannot be empty, since it must contain at least
  $\sup \emptyset$.
\end{observation}

\begin{definition}[Point-wise lifting]
Given a complete lattice $(L, \leq)$ and a set $A$, the set of all functions
from $A$ to $L$, denoted $L^A$, is usually called the \textit{point-wise
lifting} of $L$.
$(L^A, \sqsubseteq)$ is a complete lattice where $f \sqsubseteq g \iff \forall
a \in A \; f(a) \leq g(a)$.
\end{definition}

\subsection{Fixpoints}

\begin{definition}[Fixpoint]
  Given a function $f : X \to X$, a fixpoint of $f$ is an element $x \in X$ 
  such that $x = f(x)$.

  We denote the set of all fixpoints of a function as $\fix(f) = 
  \{ x \mid x \in X \mand x = f(x) \}$.
\end{definition}

Fixpoints of function will be used to describe the semantics of 
programs therefore we are interested in which conditions they exists.

\begin{definition}[Monotone function]
  Given two ordered sets $(X, \leq)$ and $(Y, \sqsubseteq)$, a function 
  $f : X \to Y$ is said to be monotone if $x \leq y \implies f(x) \sqsubseteq 
  f(y)$.
\end{definition}

The representation of program semantics as functions falls naturally in the
category of monotone functions, as different executions of the program are not
supposed to influence each other. If the semantics is not monotone, that would
mean that the program is able to distinguish between the set of executions $x$
and $y$ and perform different actions.

\begin{definition}[Least and Greatest fixpoints]
  Given a function $f : X \to X$,
  \begin{itemize}
    \item We denote the \textit{least fixpoint} as $\lfp(f)$ and is defined as
      $lfp(f) = a^* \in \fix(f)$ and $\forall a \in \fix(f) \; a^* \leq a$.
    \item We denote the \textit{greatest fixpoint} as $\gfp(f)$ and is defined as
      $gfp(f) = a^* \in \fix(f)$ and $\forall a \in \fix(f) \; a^* \geq a$.
  \end{itemize}
\end{definition}

\begin{observation}[Point-wise fixpoint]
  \label{th:pointfix}
  The least-fixpoint and greatest fixpoint on some point-wise lifted lattice on 
  a monotone function defined point-wise is the point-wise lift of the function.

  $$\lfp(\lambda p' a . f(p'(a))) = \lambda a . \lfp(\lambda p' . f(a))$$
  $$\gfp(\lambda p' a . f(p'(a))) = \lambda a . \gfp(\lambda p' . f(a))$$
\end{observation}

\begin{theorem}[Knaster-Tarski theorem]
  \label{thm:knaster}
  Let $(L, \leq)$ be a complete lattice and let $f : L \to L$ be a monotone 
  function. Then $(\text{fix}(f), \leq)$ is also a complete lattice.
\end{theorem}

We have two direct consequences: both the greatest and the least fixpoint of
$f$ exists as they are respectively top and bottom of $\fix(f)$.

\begin{theorem}[Post-fixpoint inequality]
  \label{thm:post-lfp}
  Let $f$ be a monotone function on a complete lattice then
  $$f(x) \leq x \implies \lfp(f) \leq x$$
\end{theorem}
\begin{proof}
  By theorem \ref{thm:knaster} $\lfp(f) = \bigwedge\{ y \mid y \geq f(y) \}$
  thus $\lfp(f) \leq x$ since $x \in \{ y \mid y \geq f(y) \}$.
\end{proof}

\begin{theorem}[$\lfp$ monotonicity]
  \label{thm:lfp-mono}
  Let $L$ be a complete lattice, if $P \leq Q$ and $f$ is monotone then
  $$\lfp(\lambda X. P \join f(X)) \leq \lfp(\lambda X. Q \join f(X))$$
\end{theorem}
\begin{proof}
  \begin{align*}
    P \join f(\lfp(\lambda X . Q \join f(X)))
      &\leq Q \join f(\lfp(\lambda X . Q \join f(X)))
      &\text{[Since $P \leq Q$]} \\
      &= \lfp(\lambda X . Q \join f(X))
      &\text{[By definition of fixpoint]} \\
  \end{align*}
  Thus by Theorem \ref{thm:post-lfp} pick $f = \lambda X . P \join f(X)$ and
  $x = \lfp(\lambda X. Q \join f(X))$ it follows that
  $\lfp(\lambda X. P \join f(X)) \leq \lfp(\lambda X. Q \join f(X))$.
\end{proof}

\section{Abstract Interpretation}

Abstract interpretation \cite{Cousot77, Cousot21} is the de-facto standard
approach for designing static program analysis. Fixed some representation of the
state of the program usually denoted by $\states$, the specification of a
program can be expressed as a pair of initial and final sets of states,
$\mathit{Init}, \mathit{Final} \in \pow{\states}$, and the task of verifying a
program $C$ boils down to checking if $\sem{C}(\mathit{Init}) \subseteq
\mathit{Final}$.

Clearly, this task cannot be performed in general. The solution proposed by the
framework of abstract interpretation is to construct an approximation of
$\sem{\cdot}$, usually denoted by $\sem{\cdot}^\#$, that is computable.

\subsection{Abstract Domains}

One of the techniques used by abstract interpretation to make the problem of 
verification tractable involves representing collections of states with a finite 
amount of memory.

\begin{definition}[Abstract Domain]
  A poset $(A, \leq)$ is an abstract domain of $\states$ if there exists a
  Galois insertion $\langle \pow{\states}, \subseteq \rangle
  \galoiS{\alpha}{\gamma} \langle A, \leq \rangle$.
\end{definition}

\begin{example}[Interval Domain]
  \label{exmp:interval}
  Let $\mathit{Int} = \{ [a, b] \mid a, b \in \mathbb{Z} \cup \{+\infty, -\infty \}, a 
  \leq b \} \cup \{ \bot \}$ be ordered by inclusion, each element $[a, b]$ 
  represent the set $\{ x \mid a \leq x \leq b \}$ and $\bot$ is used as a 
  representation of $\emptyset$. The structure of the 
  lattice can be summarized by the following Hasse diagram:

  \begin{center}
  \begin{tikzpicture}[scale=0.9]
    \node [] (0) at (0, 0) {$\bot$};
    \node [] (1) at (0, 1) {$[0, 0]$};
    \draw (0) to (1);
    \node [] (2) at (2, 1) {$[+1, +1]$};
    \draw (0) to (2);
    \node [] (3) at (4, 1) {$[+2, +2]$};
    \draw (0) to (3);
    \node [] (4) at (-2, 1) {$[-1, -1]$};
    \draw (0) to (4);
    \node [] (5) at (-4, 1) {$[-2, -2]$};
    \draw (0) to (5);


    \node [] (c1) at (+6, 1) {\color{black!30}$\dots$};
    \node [] (c2) at (-6, 1) {\color{black!30}$\dots$};
    
    \node [] (6) at (-3, 2) {$[-2, -1]$};
    \draw (5) to (6);
    \draw (4) to (6);
    
    \node [] (7) at (-1, 2) {$[-1, -0]$};
    \draw (4) to (7);
    \draw (1) to (7);
    
    \node [] (8) at (+1, 2) {$[0, 1]$};
    \draw (2) to (8);
    \draw (1) to (8);
    
    \node [] (9) at (+3, 2) {$[1, 2]$};
    \draw (2) to (9);
    \draw (3) to (9);

    \node [] (10) at (-2, 3) {$[-2, 0]$};
    \draw (10) to (6);
    \draw (10) to (7);
    
    \node [] (11) at (0, 3) {$[-1, +1]$};
    \draw (11) to (7);
    \draw (11) to (8);
    
    \node [] (12) at (2, 3) {$[0, +2]$};
    \draw (12) to (8);
    \draw (12) to (9);
    
    \node [] (13) at (-1, 4) {$[-2, +1]$};
    \draw (13) to (10);
    \draw (13) to (11);

    \node [] (14) at (1, 4) {$[-1, +2]$};
    \draw (14) to (11);
    \draw (14) to (12);
    
    \node [] (15) at (0, 5) {$[-2, +2]$};
    \draw (13) to (15);
    \draw (14) to (15);

    \node [] (16) at (-7, 3) {$[-\infty, -2]$};
    \node [] (17) at (-6, 4) {$[-\infty, -1]$};
    \draw (16) to (17);
    \node [] (18) at (-5, 5) {$[-\infty, 0]$};
    \draw (17) to (18);

    \node [] (b1) at (-4, 4) {};
    \draw [loosely dotted] (b1) to (18);
    \node [] (b2) at (-5, 3) {};
    \draw [loosely dotted] (b2) to (17);
    \node [] (b3) at (-6, 2) {};
    \draw [loosely dotted] (b3) to (16);
    
    \node [] (19) at (+7, 3) {$[+2, +\infty]$};
    \node [] (20) at (+6, 4) {$[+1, +\infty]$};
    \draw (19) to (20);
    \node [] (21) at (+5, 5) {$[0, +\infty]$};
    \draw (20) to (21);


    \node [] (a1) at (+4, 4) {};
    \draw [loosely dotted] (a1) to (21);
    \node [] (a2) at (+5, 3) {};
    \draw [loosely dotted] (a2) to (20);
    \node [] (a3) at (+6, 2) {};
    \draw [loosely dotted] (a3) to (19);

    \node (22) at (0, 8) {$[-\infty, +\infty]$};

    \node (25) at (-5, 2) {};
    \draw[loosely dotted] (25) to (5);
    \node (26) at (+5, 2) {};
    \draw[loosely dotted] (26) to (3);
    
    \node (27) at (-4, 3) {};
    \draw[loosely dotted] (27) to (6);
    \node (28) at (+4, 3) {};
    \draw[loosely dotted] (28) to (9);
    
    \node (29) at (-3, 4) {};
    \draw[loosely dotted] (29) to (10);
    \node (30) at (+3, 4) {};
    \draw[loosely dotted] (30) to (12);
    
    \node (31) at (-2, 5) {};
    \draw[loosely dotted] (31) to (13);
    \node (32) at (+2, 5) {};
    \draw[loosely dotted] (32) to (14);
    
    \node (33) at (-1, 6) {};
    \draw[loosely dotted] (33) to (15);
    \node (34) at (1, 6) {};
    \draw[loosely dotted] (34) to (15);

    \node (35) at (0, 7) {};
    \draw[loosely dotted] (35) to (22);
    \node (a1) at (-1, 7) {};
    \draw[loosely dotted] (a1) to (22);
    \node (a2) at (+1, 7) {};
    \draw[loosely dotted] (a2) to (22);

    \node (36) at (-4, 6) {};
    \draw[loosely dotted] (36) to (18);
    
    \node (37) at (+4, 6) {};
    \draw[loosely dotted] (37) to (21);

    \node (38) at (-8, 2) {};
    \draw[loosely dotted] (38) to (16);
    
    \node (39) at (+8, 2) {};
    \draw[loosely dotted] (39) to (19);

  \end{tikzpicture}
  \end{center}


  Then, there is a Galois insertion from $\mathit{Int}$ to $\pow{\mathbb{Z}}$ defined as:
  $$\gamma(A) = \begin{cases}
    \{ x \mid a \leq x \leq b \} & \text{if } A = [a, b] \\
    \emptyset & \text{otherwise}
  \end{cases}$$
  $$\alpha(C) = \begin{cases}
    [\min C, \max C] & \text{if } C \neq \emptyset \\
    \bot & \text{otherwise}
  \end{cases}$$
\end{example}

\begin{example}[Complete sign domain]
  \label{exmp:sign}
  Let $Sign = \{ \bot , <0, >0, =0, \leq 0, \neq 0, \geq 0, \mathbb{Z}\}$ be 
  ordered by following the Hasse diagram below.

  \begin{center}
  \begin{tikzpicture}
    \node [] (0) at (0, 0) {$\bot$};

    \node [] (1) at (-1, 1) {$< 0$};
    \draw (0) to (1);
    \node [] (2) at (0, 1) {$=0$};
    \draw (0) to (2);
    \node [] (3) at (+1, 1) {$> 0$};
    \draw (0) to (3);
    
    \node [] (4) at (-1, 2) {$\leq 0$};
    \draw (1) to (4);
    \draw (2) to (4);
    \node [] (5) at (0, 2) {$\neq 0$};
    \draw (1) to (5);
    \draw (3) to (5);
    \node [] (6) at (+1, 2) {$\geq 0$};
    \draw (2) to (6);
    \draw (3) to (6);
    
    \node [] (7) at (0, 3) {$\mathbb{Z}$};
    \draw (6) to (7);
    \draw (5) to (7);
    \draw (4) to (7);
  \end{tikzpicture}
  \end{center}

  Then, there is a Galois insertion from $Sign$ to $\pow{\mathbb{Z}}$ defined as:
  $$\gamma(A) = \begin{cases}
    \{ x \mid x \;op\; 0 \} & \text{if } A = op\;0 \\
    \mathbb{Z}              & \text{if } A = \mathbb{Z} \\
    \emptyset & \text{otherwise}
  \end{cases}$$
  $$\alpha(C) = \begin{cases}
    \bot & \text{if } C = \emptyset \\
    op \; 0 & \text{if } C \subseteq \{ x \mid x \; op \; 0 \}
        \mand op \in \{<, >, =, \leq, \geq, \neq \} \\
    \mathbb{Z} & \text{otherwise}
  \end{cases}$$
\end{example}

The fundamental goal of abstract interpretation is to provide an approximation 
of the non-computable aspects of program semantics. The core concept is captured 
by the definition of soundness:

\begin{definition}[Soundness]
  Given an abstract domain $A$, an abstract function $f^\# : A \to A$ is a 
  sound approximation of a concrete function $f : \pow{\states} \to 
  \pow{\states}$ if
  $$\alpha(f(P)) \leq f^\#(\alpha(P))$$
\end{definition}

Hence, the goal of abstract interpretation is to construct a sound 
over-approximation of the program semantics that is computable (efficiently).

\begin{example}
  We can use the sign domain to construct a sound approximation of the
  multiplication operation: 
  \begin{table}[h!]
    \centering
    \begin{tabular}{|c|c|c|c|c|c|c|c|c|}
      \hline
      $\times^\#$ & $\bot$ & $< 0$ & $> 0$ & $= 0$ & $\le 0$ & $\ne 0$ & $\ge 0$ 
                  & $\mathbb{Z}$ \\
      \hline
      $\bot$ & $\bot$ & $\bot$ & $\bot$ & $\bot$ & $\bot$ & $\bot$ & $\bot$ 
             & $\bot$ \\
      \hline
      $< 0$ & $\bot$ & $> 0$ & $< 0$ & $= 0$ & $< 0$ & $\ne 0$ & $\le 0$ 
            & $\mathbb{Z}$ \\
      \hline
      $> 0$ & $\bot$ & $< 0$ & $> 0$ & $= 0$ & $\le 0$ & $\ne 0$ & $\ge 0$ 
            & $\mathbb{Z}$ \\
      \hline
      $= 0$ & $\bot$ & $= 0$ & $= 0$ & $= 0$ & $= 0$ & $= 0$ & $= 0$ & $= 0$ \\
      \hline
      $\le 0$ & $\bot$ & $< 0$ & $\le 0$ & $= 0$ & $\le 0$ & $\ne 0$ & $\le 0$ 
              & $\mathbb{Z}$ \\
      \hline
      $\ne 0$ & $\bot$ & $\ne 0$ & $\ne 0$ & $= 0$ & $\ne 0$ & $\ne 0$ 
              & $\ne 0$ & $\mathbb{Z}$ \\
      \hline
      $\ge 0$ & $\bot$ & $\le 0$ & $\ge 0$ & $= 0$ & $\le 0$ & $\ne 0$ 
              & $\ge 0$ & $\mathbb{Z}$ \\
      \hline
      $\mathbb{Z}$ & $\bot$ & $\mathbb{Z}$ & $\mathbb{Z}$ & $= 0$ 
                   & $\mathbb{Z}$ & $\mathbb{Z}$ & $\mathbb{Z}$ & $\mathbb{Z}$ \\
      \hline
    \end{tabular}
    \caption{Multiplication table for $Sign$ domain}
  \end{table}
\end{example}
\chapter{The abstract Hoare logic framework}


In this chapter, we will develop the basic theory of \textit{Abstract Hoare
Logic}. We will formalize the extensible language $\lang$, a minimal imperative
programming language that is parametric on a set of basic commands to permit
the definition of arbitrary program features, such as pointers, objects, etc.
We will define the semantics of the language, provide the standard definition
of Hoare triples, and introduce the concept of abstract inductive semantics; a
modular approach to express the strongest postcondition of a program, where the
assertion language is a complete lattice. Additionally, we will present a sound
and complete proof system to reason about these properties.

\section{The $\lang$ programming language}

\subsection{Syntax}

The $\lang$ language is inspired by Dijkstra's guarded command languages
\cite{Dijkstra74} with the goal of being as general as possible by being
parametric on a set of \textit{basic commands}. The $\lang$ language is general
enough to describe any imperative non-deterministic programming language.

\begin{definition}[$\lang$ language syntax]
  Given a set $\mathit{BCmd}$ of basic commands, the set on valid $\lang$ programs is 
  defined by the following inductive definition:

  \begin{align*}
    b \in \mathit{BCmd} \\
    \lang \ni C, C_1, C_2 \; & \cceq \sskip        & \text{Skip}\\
                             & \smid b             & \text{Basic command}\\
                             & \smid C_1 \fcmp C_2 & \text{Program composition}\\
                             & \smid C_1 + C_2     & \text{Non deterministic choice}\\
                             & \smid C^\fix        & \text{Iteration}\\
  \end{align*}
\end{definition}

\begin{example} \label{exmp:base-commands-syntax}
  Usually the set of basic commands contains a command to perform tests $e ?$
  discarding executions that do not satisfy the predicate $e$, and $x \ass v$
  to assign the value $v$ to the variable $x$.
\end{example}

\subsection{Semantics}

Fixed a set $\states$ of states (usually a collection of associations between
variables names and values) and a family of partial functions $\bsem{\cdot} :
\mathit{BCmd} \to \states \topartial \states$ we can define the denotational semantics
of programs in $\lang$. The \textit{collecting semantics} is defined as a function
$\sem{\cdot} : \lang \to \pow{\states} \to \pow{\states}$ that associates a
program $C$ and a set of initial states to the set of states reached after
executing the program $C$ from the initial states, this is also know as the
predicate transformer semantics \cite{Dijkstra74}.

\begin{definition}[Denotational semantics]
  \label{def:deno}
  Given a set $\states$ of states and a family of partial functions
  $\bsem{\cdot} : \mathit{BCmd} \to \states \topartial \states$ the denotational
  semantics is defined as follows:

  \begin{align*}
      \sem{\cdot}         & \;\;:\; \lang \to \pow{\states} \to \pow{\states} \\
      \sem{\sskip}        &\defeq id \\
      \sem{b}             &\defeq \lambda P . \{ \bsem{b}(p)\; \mid 
      p \in P \mand \bsem{b}(p) \downarrow\} \\
      \sem{C_1 \fcmp C_2} &\defeq \sem{C_2} \circ \sem{C_1} \\
      \sem{C_1 + C_2}     &\defeq \lambda P . \sem{C_1} P \cup \sem{C_2} P \\
      \sem{C^\fix}        &\defeq \lambda P . \lfp(\lambda P'. P \cup \sem{C} P')
  \end{align*}
  
  Where the notation $\bsem{b}(p)\downarrow$ is used to denote that $\bsem{b}$
  is defined on input $p$.
\end{definition}


\begin{example}
  We can define the semantics of the basic commands introduced in 
  \ref{exmp:base-commands-syntax} as:
  $$\bsem{e ?}(\sigma) \defeq \begin{cases}
    \; \sigma & \sigma \models e \\
    \; \uparrow & otherwise
  \end{cases}$$

  Where $\sigma \models e$ means that the state $\sigma$ satisfies the 
  predicate $e$ and $\uparrow$ is denoting that the function is diverging.

  $$\bsem{x \ass e}(\sigma) \defeq \sigma[eval(e, \sigma)/x]$$
  Where $eval$ is some evaluate function for the expressions on the left-hand
  side of assignments and then is substitute in place of $x$ in the 
  state $\sigma$.
\end{example}

\begin{theorem}[Monotonicity]
  \label{thm:sem-mono}
  $\forall \; C \in \lang$ $\sem{C}$ is well-defined and monotone.
\end{theorem}
\begin{proof}
  We want to prove that $\forall P, Q \in \pow{\states}$ and $C \in \lang$
  $$P \subseteq Q \implies \sem{C}(P) \subseteq \sem{C}(Q)$$
  By structural induction on $C$:
  \begin{itemize}
    \item $\sskip$:
      \begin{align*}
        \sem{\sskip}(P) 
          &= P
          & \text{[By definition of $\sem{\sskip}$]}\\
          &\subseteq Q \\
          &= \sem{\sskip}(Q) 
          & \text{[By definition of $\sem{\sskip}$]}\\
      \end{align*}

    \item $b$:
      \begin{align*}
        \sem{b}(P) 
          &= \{ \bsem{b}(x)\downarrow \; \mid x \in P \} 
          & \text{[By definition of $\sem{b}$]}\\
          &\subseteq \{ \bsem{b}(x)\downarrow \; \mid x \in Q \} 
          & \text{[Since $P \subseteq Q$]}\\
          &= \sem{b}(Q) 
          & \text{[By definition of $\sem{b}$]}\\
      \end{align*}

    \item $C_1 \fcmp C_2$:

      By inductive hypothesis $\sem{C_1}$ is monotone hence
      $\sem{C_1}(P) \subseteq \sem{C_2}(Q)$

      \begin{align*}
        \sem{C_1 \fcmp C_2}(P) 
          &= \sem{C_2}(\sem{C_1}(P))
          &\text{[By definition of $\sem{C_1 \fcmp C_2}$]}\\
          &\subseteq \sem{C_2}(\sem{C_1}(Q))
          &\text{[By inductive hypothesis on $\sem{C_2}$]} \\
      \end{align*}
  
    \item $C_1 + C_2$:
      \begin{align*}
        \sem{C_1 + C_2}(P) 
          &= \sem{C_1}(P) \cup \sem{C_2}(P)
          &\text{[By definition of $\sem{C_1 + C_2}$]}\\
          &\subseteq \sem{C_1}(Q) \cup \sem{C_2}(P)
          &\text{[By inductive hypothesis on $\sem{C_1}$]} \\
          &\subseteq \sem{C_1}(Q) \cup \sem{C_2}(Q)
          &\text{[By inductive hypothesis on $\sem{C_2}$]} \\
          &= \sem{C_1 + C_2}(Q) 
          &\text{[By definition of $\sem{C_1 + C_2}$]}\\
      \end{align*}
    
    \item $C^\fix$:

      \begin{align*}
        \sem{C^\fix}(P) 
          &\text{[By definition of $\sem{C^\fix}$]}\\
          &= \lfp(\lambda P'. P \cup \sem{C}(P'))
          &\subseteq \lfp(\lambda P'. Q \cup \sem{C}(P'))
          &\text{[By Theorem \ref{thm:lfp-mono}]}\\
          &= \sem{C^\fix}(Q) 
          &\text{[By definition of $\sem{C^\fix}$]}\\
      \end{align*}
      
      Clearly all the $\lfp$ are well-defined since by inductive hypothesis
      $\sem{C}$ is monotone and $\pow{\states}$ is a complete from 
      \ref{thm:knaster} the least-fixpoint exists.
  \end{itemize}

\end{proof}

\begin{observation}
  As observed in \cite{Fischer79} when the set of basic commands contains a 
  command to discard executions we can define the usual deterministic control 
  flow commands as syntactic sugar.

  $$\mathbf{if} \; b \; \mathbf{then} \; C_1 \; \mathbf{else} \; C_2 \defeq (b ? \fcmp C_1) 
  + (\neg b ? \fcmp C_2)$$
  $$\mathbf{while} \; b \; \mathbf{do} \; C \defeq (b? \fcmp C)^\fix \fcmp \neg b ?$$
\end{observation}

\begin{observation}
  Regular languages of Kleene algebras \cite{Kozen97} usually provide an
  iteration command usually denoted $C^\star$ whose semantics is
  $\sem{C^\star}(P) \defeq \bigcup_{n \in \nat} \sem{C}^n(P)$. This is
  equivalent to $C^\fix$, the reason why a fixpoint formulation was
  chosen will become clear in \ref{obs:abstract-fix}.
\end{observation}

\begin{example}
  Let $C \defeq (x \leq 10? \fcmp x := x + 1)^\fix + (x := 55)$ and 
  $P = \{ x = 1 \}$ then we can compute $\sem{C}(P)$ as:
  \begin{align*}
    \sem{C}(P)
      &= \sem{(x \leq 10? \fcmp x := x +1)^\fix}(P) \cup \sem{x := 55}(P) \\
      &= \lfp(\lambda P' . P \cup \sem{x \leq 10? \fcmp x := x + 1}(P'))
        \cup \{x = 55\} \\
      &= \{ x \in \{1, ..., 10\} \} \cup \{x = 55\} \\
      &= \{ x \in \{1, ..., 10, 55\} \}
  \end{align*}
\end{example}


\section{Abstract inductive semantics}

From the theory of abstract interpretation we know that the definition of the
denotational semantics can be modified to work on any complete lattice as long
as we provide suitable function for the basic commands. The rationale
behind is the same as in the denotational semantics but instead of representing
collections of states with $\pow{\states}$ now they are represented in an
arbitrary complete lattice.

\begin{definition}[Abstract inductive semantics]

  \label{def:abstract-inductive-semantics}
  Given a complete lattice $A$ and a family of monotone functions $\bsem{\cdot}^A : 
  \mathit{BCmd} \to A \to A$ the abstract inductive semantics is defined inductively as 
  follows:

  \begin{align*}
      \asem{\cdot}         & \;\;:\; \lang \to A \to A \\
      \asem{\sskip}         &\defeq id \\
      \asem{b}             &\defeq \bsem{b}^A \\
      \asem{C_1 \fcmp C_2} &\defeq \asem{C_2} \circ \asem{C_1} \\
      \asem{C_1 + C_2}     &\defeq \lambda P . \asem{C_1} P \join_A \asem{C_2} P \\
      \asem{C^\fix}        &\defeq \lambda P . \lfp(\lambda P'. P \join_A \asem{C} P')
  \end{align*}
\end{definition}


When designing abstract interpreters to perform abstract interpretation,
iterative commands are usually not expressed directly as fixpoints but by
some over-approximation, as is the case for the $C^\fix$ command. This is
necessary since the goal of the abstract interpreter is to be executed and, in
general, if the lattice on which the interpretation executed run has infinite
ascending chains, its computation can diverge. In our case, the termination
requirement is not necessary since we are not interested in computing the abstract
inductive semantics but using it as a reference on which the definition of
abstract Hoare logic is dependent.


As we did for the concrete collecting semantics, we need to prove that the
semantics is well-defined. In general, For this we require for $A$
to be a complete lattice or for $\bsem{b}$ to be monotone, play an essential role
as they guarantee the existence of the required least-fixpoint.

\begin{theorem}[Monotonicity]
  \label{thm:asem-mono} 
  $\forall \; C \in \lang$ $\asem{C}$ is well-defined and monotone.
\end{theorem}
\begin{proof}
  We want to prove that $\forall P, Q \in A$ and $C \in \lang$
  $$P \leq_A Q \implies \asem{C}(P) \leq_A \asem{C}(Q)$$
  By structural induction on $C$:
  \begin{itemize}
    \item $\sskip$:
      \begin{align*}
        \asem{\sskip}(P) 
          &= P 
          & \text{[By definition of $\asem{\sskip}$]}\\
          &\leq Q \\
          &= \asem{\sskip}(Q) 
          & \text{[By definition of $\asem{\sskip}$]}\\
      \end{align*}

    \item $b$:
      \begin{align*}
        \asem{b}(P) 
          &= \bsem{b}^A(P)
          & \text{[By definition of $\asem{b}$]}\\
          &\leq \bsem{b}^A(Q)
          & \text{[By definition]}\\
          &= \asem{b}(Q) 
          & \text{[By definition of $\asem{b}$]}\\
      \end{align*}

    \item $C_1 \fcmp C_2$:

      By inductive hypothesis $\asem{C_1}$ is monotone hence
      $\asem{C_1}(P) \leq_A \asem{C_1}(Q)$

      \begin{align*}
        \asem{C_1 \fcmp C_2}(P) 
          &= \asem{C_2}(\asem{C_1}(P))
          &\text{[By definition of $\asem{C_1 \fcmp C_2}$]}\\
          &\leq_A \asem{C_2}(\asem{C_1}(Q))
          &\text{[By inductive hypothesis on $\asem{C_2}$]} \\
      \end{align*}
  
    \item $C_1 + C_2$:
      \begin{align*}
        \asem{C_1 + C_2}(P) 
          &= \asem{C_1}(P) \join_A \asem{C_2}(P)
          &\text{[By definition of $\asem{C_1 + C_2}$]}\\
          &\leq_A \asem{C_1}(Q) \join_A \asem{C_2}(P)
          &\text{[By inductive hypothesis on $\asem{C_1}$]} \\
          &\leq_A \asem{C_1}(Q) \join_A \asem{C_2}(Q)
          &\text{[By inductive hypothesis on $\asem{C_2}$]} \\
          &= \asem{C_1 + C_2}(Q) 
          &\text{[By definition of $\asem{C_1 + C_2}$]}\\
      \end{align*}
    
    \item $C^\fix$:

      \begin{align*}
        \asem{C^\fix}(P) 
          &= \lfp(\lambda P'. P \join_A \asem{C}(P'))
          &\text{[By definition of $\asem{C^\fix}$]}\\
          &\text{[By Theorem \ref{thm:lfp-mono}]}\\
          &\leq_A \lfp(\lambda P'. Q \join_A \asem{C}(P'))
          &= \asem{C^\fix}(Q) 
          &\text{[By definition of $\asem{C^\fix}$]}\\
      \end{align*}
  \end{itemize}


  Clearly all the $\lfp$ are well-defined since by inductive hypothesis
  $\sem{C}$ is monotone and $A$ is a complete from 
  \ref{thm:knaster} the least-fixpoint exists.
\end{proof}

From now on we will refer to the complete lattice $A$ used to define the abstract
inductive semantics as \textit{domain} borrowing the terminology from abstract
interpretation.

\begin{observation}
  \label{obs:post}
  When picking as a domain the lattice $\pow{\states}$ and as basic commands
  $\bsem{b}^{\pow{\states}}(P) = \{ \bsem{b}(\sigma)\downarrow \; \mid \sigma 
  \in P \}$ we will obtain the denotational semantics from the 
  abstract inductive semantics, that is: $\forall \; C \in \lang$ $\forall P \in 
  \pow{\states}$ 
  $$\asem[\pow{\states}]{C}(P) = \sem{C}(P)$$
  This can be easily checked by comparing the two definitions.
\end{observation}

From this observation, we can see that Theorem \ref{thm:sem-mono} is just an
instance of Theorem \ref{thm:asem-mono} since $\pow{\states}$ is a
complete lattice and the semantics of the basic commands is monotone by
construction.

\subsection{Connection with Abstract Interpretation}

As stated above, the definition of abstract inductive semantics is closely
related to the one of abstract semantics \cite{Cousot77}. In particular, the 
definition of abstract inductive semantics, when the semantics of the basic
commands is sound, is equivalent to an abstract semantics.

\begin{theorem}[Abstract interpretation instance]
  \label{thm:sound-ai}
  If $A$ is an abstract domain and $\bsem{\cdot}^A$ is a sound 
  over-approximation of $\bsem{\cdot}$, then $\asem{\cdot}$ is a sound 
  over-approximation of $\sem{\cdot}$.
\end{theorem}
\begin{proof}
  We prove $\alpha(\sem{C}(P)) \leq \asem{C}(\alpha(P))$ by structural
  induction on $C$:

  \begin{itemize}
    \item $\sskip$:
      \begin{align*}
        \alpha(\sem{\sskip}(P))
          &= \alpha(P)
          & \text{[By definition of $\sem{\sskip}$]}\\
          &= \asem{\sskip}(\alpha(P)) 
          & \text{[By definition of $\asem{\sskip}$]}\\
      \end{align*}

    \item $b$:
      \begin{align*}
        \alpha(\sem{b}(P))
          &= \bsem{b}(P)
          & \text{[By definition of $\sem{b}$]}\\
          &\leq \bsem{b}^A(\alpha(P))
          & \text{[By definition]}\\
          &= \asem{b}(\alpha(P)) 
          & \text{[By definition of $\asem{b}$]}\\
      \end{align*}

    \item $C_1 \fcmp C_2$:

      \begin{align*}
        \alpha(\sem{C_1 \fcmp C_2}(P))
          &= \alpha(\sem{C_2}(\sem{C_1}(P)))
          &\text{[By definition of $\sem{C_1 \fcmp C_2}$]}\\
          &\leq \asem{C_2}(\alpha(\sem{C_1}(P)))
          &\text{[By inductive hypothesis on $C_2$]}\\
          &\leq \asem{C_2}(\asem{C_1}(\alpha(P)))
          &\text{[By inductive hypothesis on $C_1$} \\
          && \text{and $\asem{C_2}$ monotone]}\\
          &= \asem{C_1 \fcmp C_2}(\alpha(P))
          &\text{[By definition of $\asem{C_1 \fcmp C_2}$]}\\
      \end{align*}
  
    \item $C_1 + C_2$:
      \begin{align*}
        \alpha(\sem{C_1 + C_2}(P))
          &= \alpha(\sem{C_1}(P) \cup \sem{C_2}(P))
          &\text{[By definition of $\sem{C_1 + C_2}$]}\\
          &\leq \alpha(\sem{C_1}(P)) \join \alpha(\asem{C_2}(P)) \\
          &\leq \asem{C_1}(\alpha(P)) \join \asem{C_2}(\alpha(P))
          &\text{[By inductive hypothesis on $C_1$} \\
          && \text{and $C_2$]} \\
          &= \asem{C_1 + C_2}(\alpha(P))
          &\text{[By definition of $\asem{C_1 + C_2}$]}\\
      \end{align*}
    
    \item $C^\fix$:

      \begin{align*}
        \alpha(\sem{C^\fix}(P) )
          &= \alpha(\lfp(\lambda P'. P \cup \sem{C}(P')))
          &\text{[By definition of $\sem{C^\fix}$]}\\
          &= \alpha(\bigcup_{n \in \mathbb{N}}{\sem{C}^n(P)}) \\
          &\leq \bigvee_{n \in \mathbb{N}}{\alpha(\sem{C}^n(P))}) \\
          &\leq \bigvee_{n \in \mathbb{N}}{(\asem{C})^n(\alpha(P))}
          &\text{[By inductive hypothesis on $C$]}\\
          &\leq \lfp(\lambda P'. \alpha(P) \join \asem{C}(P')) \\
          &= \asem{C^\fix}(\alpha(P)) 
          &\text{[By definition of $\asem{C^\fix}$]}\\
      \end{align*}
  \end{itemize}
\end{proof}

This connection also allows us to obtain abstract inductive semantics through 
Galois insertions.

\begin{definition}[Abstract Inductive Semantics by Galois Insertion]
  \label{def:aisgi}
  Let $\langle C, \sqsubseteq \rangle \galoiS{\alpha}{\gamma} \langle A, \leq
  \rangle$ be a Galois insertion, and let $\asem[C]{C}$ be some abstract
  inductive semantics defined on $C$. Then, the abstract inductive semantics
  defined on $A$ with $\bsem{b}^A \defeq \alpha \circ \bsem{b}^C \circ \gamma$
  is the abstract inductive semantics obtained by the Galois insertion between
  $C$ and $A$.
\end{definition}

The abstract inductive semantics obtained by Galois insertion between 
$\pow{\states}$ and any domain $A$ can be seen as the best abstract inductive 
interpreter on $A$.

\begin{observation}
  \label{obs:abstract-fix}
  There are some domains where $\exists \; C \in \lang$ such that
  $\bigvee_{n \in \nat} (\asem{C})^n(P) \neq \lfp(\lambda P'. P \join_A
  \asem{C}(P'))$.
\end{observation}
\begin{example}
  Let $C \defeq (x > 1? \fcmp ((even(x) ? \fcmp X := x + 3) +
  (\neg even(x)? \fcmp x := x - 2))^\fix$ when performing the computation on
  the interval domain, if we compute $C$ using the infinitary join:
  \begin{align*}
    \asem{C^\star}([5, 5])
      &= \bigvee_{n \in \mathbb{N}} (\asem{x > 1? \fcmp ((even(x) ? \fcmp x :=
        x + 3) + (\neg even(x)? \fcmp x := x - 2))})^n([5, 5]) \\
      &= [5, 5] \join [3, 3] \join [1, 1] \join \bot \join \bot ... \\
      &= [1, 5]
  \end{align*}

  Instead using the least-fixpoint:
  \begin{align*}
    \asem{C^\fix}([5, 5])
      &= \lfp(\lambda P' . [5, 5] \join \asem{x > 1? \fcmp ((even(x) ? \fcmp x :=
        x + 3) + (\neg even(x)? \fcmp x := x - 2))}(P')) \\
      &= [-\infty, +\infty]
\end{align*}

  The difference is caused by the fact that when we are computing the infinite 
  join, all the joins happen after executing the semantics of the loop body, 
  instead, when using the least-fixpoint formulation the join is performed 
  before executing the the semantics of the body.
  
\end{example}
\section{Abstract Hoare Logic}
\label{chp:intro-ahorare}

\subsection{Hoare logic}
Hoare logic  \cite{Hoare69, Floyd93} was one of the first methods designed for 
the verification of programs, Its core concept is that of partial correctness 
assertions. A Hoare triple is a formula $\htriple{P}{C}{Q}$ where $P$ and $Q$ are 
assertions on the initial and final states of a program $C$, respectively. 
These assertions are partial in the sense that $Q$ is meaningful only when the 
execution of $C$ on $P$ terminates.

Hoare logic is designed as a proof system, where the syntax 
$\vdash \htriple{P}{C}{Q}$ indicates that the triple 
$\htriple{P}{C}{Q}$ is proved by applying the rules of the proof system.

The original formulation of Hoare logic was given for an imperative language 
with deterministic constructs, but it can be easily defined for our language 
$\lang$ following the work in \cite{Moller21}.

\begin{definition}[Hoare triple]
  \label{def:hoare}
  Fixed the semantics of the basic commands, an Hoare triple denoted by 
  $\htriple{P}{C}{Q}$, is valid if and only if $\sem{C}(P) \subseteq Q$.

  $$\models \htriple{P}{C}{Q} \iff \sem{C}(P) \subseteq Q$$
\end{definition}

We will use the syntax $\models \htriple{P}{C}{Q}$ to refer to valid triples,
$\not \models \htriple{P}{C}{Q}$ to refer to invalid triples.

\begin{example}[Hoare triples]
  \label{exmp:hlogic}
We have that $\htriple{x \in [1, 2]}{x := x + 1}{x \in [2, 4]}$, is a
valid triple since from any state in which either $x = 1$ or $x = 2$,
incrementing by one the value of $x$ leads to states in which $x$ is either $2$
or $3$. Specifically, starting from $x = 1$ leads us to $x = 2$ and starting
from $x = 2$ leads us to $x = 3$.

Since the conclusion of Hoare triples must contain all the final states, the
triple $\htriple{P}{C}{\top}$ is always valid since $\top$ contains all the
possible states.

An example of an invalid triple is $\htriple{x \in [1, 2]}{x := x
+ 1}{x \in [1, 2]}$ since the state $x = 2$ satisfies the precondition and
executing the program on it results in the state $x = 3$, which does not satisfy
$x \in [1, 2]$.

Since Hoare logic is concerned only with termination, when the program is
non-terminating, we can prove any property. For example, $\htriple{x
\in [0, 10]}{(x \leq 20? \fcmp x := x - 1)^\fix \fcmp x \geq 20?}{Q}$ is always
a valid triple since the program is non-terminating for any $x \in [0, 10]$. 
The set of reachable states is empty, thus the postcondition is vacuously true.

This is the reason why Hoare logic is called a partial correctness logic,
where partial means that it can prove the adherence of a program to
some specification only when it is terminating. The termination of the program
must be proved by resorting to some alternative method.
\end{example}

\begin{definition}[Hoare logic]$\;$ \\
  \label{def:hoaretules}
  The rules of Hoare logic are defined as follows:
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(\sskip)$}
    \UnaryInfC{$\vdash \htriple{P}{\sskip}{P}$}
  \end{prooftree}

  % Rule for a basic command
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(base)$}
    \UnaryInfC{$\vdash \htriple{P}{b}{\bsem{b}(P)}$}
  \end{prooftree}

  % Rule for sequential composition
  \begin{prooftree}
    \AxiomC{$\vdash \htriple{P}{C_1}{Q}$}
    \AxiomC{$\vdash \htriple{Q}{C_2}{R}$}
    \RightLabel{$(seq)$}
    \BinaryInfC{$\vdash \htriple{P}{C_1 \fcmp C_2}{R}$}
  \end{prooftree}

  % Rule for nondeterministic choice
  \begin{prooftree}
    \AxiomC{$\vdash \htriple{P}{C_1}{Q}$}
    \AxiomC{$\vdash \htriple{P}{C_2}{Q}$}
    \RightLabel{$(disj)$}
    \BinaryInfC{$\vdash \htriple{P}{C_1 + C_2}{Q}$}
  \end{prooftree}

  \begin{prooftree}
    \AxiomC{$\vdash \htriple{P}{C}{P}$}
    \RightLabel{$(iterate)$}
    \UnaryInfC{$\vdash \htriple{P}{C^\fix}{P}$}
  \end{prooftree}

  % Rule for strengthening the precondition and weakening the postcondition
  \begin{prooftree}
    \AxiomC{$P \subseteq P'$}
    \AxiomC{$\vdash \htriple{P'}{C}{Q'}$}
    \AxiomC{$Q' \subseteq Q$}
    \RightLabel{$(consequence)$}
    \TrinaryInfC{$\vdash \htriple{P}{C}{Q}$}
  \end{prooftree}
\end{definition}

The proof system described in Definition \ref{def:hoaretules} is logically
sound, meaning that all its provable triples are valid with respect to
Definition \ref{def:hoare}.

\begin{theorem}[Soundness]
  $$\vdash \htriple{P}{C}{Q} \implies \models \htriple{P}{C}{Q}$$
\end{theorem}

As observed by Cook \cite{Cook78}, the reverse implication is not true, in 
general, as a consequence of Gödel's incompleteness theorem. For this reason, 
Cook developed the concept of relative completeness, in which all the instances 
of $\subseteq$ are provided by an oracle, proving that the incompleteness of the 
proof system is only caused by the incompleteness of the assertion language.

\begin{theorem}[Relative completeness]
  \label{thm:hlogic-complete}
  $$\models \htriple{P}{C}{Q} \implies \vdash \htriple{P}{C}{Q}$$
\end{theorem}

\subsection{Abstracting Hoare logic}
The idea of designing a Hoare-like logic to reason about properties of programs
expressible within the theory of lattices using concepts from abstract
interpretation is not new. In fact, \cite{Cousot12} already proposed a
framework to perform this kind of reasoning. However, the validity of the
triples in \cite{Cousot12} depends on the standard definition of Hoare
triples, and the proof system is incomplete if we ignore the rule to embed
standard Hoare triples in the abstract ones.

Our approach will be different. In particular, the meaning of abstract Hoare 
triples will be dependent on the abstract inductive semantics, and we will 
provide a sound and (relatively) complete without resorting to embedding Hoare 
logic in its proof system as \cite{Cousot12}.

\begin{definition}[Abstract Hoare triple]
  \label{def:aht}
  Given an abstract inductive semantics $\asem{\cdot}$ on the complete lattice
  $A$, the abstract Hoare triple written $\atriple{P}{C}{Q}$ is valid if
  and only if $\asem{C}(P) \leq_A Q$.

  $$\models \atriple{P}{C}{Q} \iff \asem{C}(P) \leq_A Q$$
\end{definition}

The definition is equivalent to the Definition \ref{def:hoare} 
but here a generic abstract inductive semantics is used to provide the strongest 
postcondition of programs.

In Abstract Hoare logic some of the examples shown in example \ref{exmp:hlogic} 
still hold, in particular we have that:
\begin{example}
  $$\models \atriple{P}{C}{\top}$$
\end{example}
\begin{proof}
  \begin{align*}
    \models \atriple{P}{C}{\top}
      & \iff \asem{C}(P) \leq \top & \text{By definition of $\atriple{\cdot}{\cdot}{\cdot}$} \\
  \end{align*}

  And since $\top$ is the top element of $A$ we have $\top \geq \asem{C}(P)$
\end{proof}

\subsubsection{2.3.3 Proof system}
As per Hoare logic we will provide a sound and relatively complete (in the sense
of \cite{Cook78}) proof system to derive abstract Hoare triples in a 
compositional fashion.

\begin{definition}[Abstract Hoare rules]$\;$\\
  \label{def:ahtrules}
  % Rule for the identity command
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(\sskip)$}
    \UnaryInfC{$\vdash \atriple{P}{\sskip}{P}$}
  \end{prooftree}

  % Rule for a basic command
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple{P}{b}{\bsem{b}^A(P)}$}
  \end{prooftree}

  % Rule for sequential composition
  \begin{prooftree}
    \AxiomC{$\vdash \atriple{P}{C_1}{Q}$}
    \AxiomC{$\vdash \atriple{Q}{C_2}{R}$}
    \RightLabel{$(\mathbb{\fcmp})$}
    \BinaryInfC{$\vdash \atriple{P}{C_1 \fcmp C_2}{R}$}
  \end{prooftree}

  % Rule for nondeterministic choice
  \begin{prooftree}
    \AxiomC{$\vdash \atriple{P}{C_1}{Q}$}
    \AxiomC{$\vdash \atriple{P}{C_2}{Q}$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple{P}{C_1 + C_2}{Q}$}
  \end{prooftree}

  % Rule for iteration (Kleene star)
  \begin{prooftree}
    \AxiomC{$\vdash \atriple{P}{C}{P}$}
    \RightLabel{$(\fix)$}
    \UnaryInfC{$\vdash \atriple{P}{C^\fix}{P}$}
  \end{prooftree}

  % Rule for strengthening the precondition and weakening the postcondition
  \begin{prooftree}
    \AxiomC{$P \leq P'$}
    \AxiomC{$\vdash \atriple{P'}{C}{Q'}$}
    \AxiomC{$Q' \leq Q$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple{P}{C}{Q}$}
  \end{prooftree}
\end{definition}

The rules can be summarized as:
\begin{itemize}
  \item The identity command does not change the state, so if $P$ holds before,
    it will hold after the execution.

  \item For a basic command $b$, if $P$ holds before the execution, then 
    $\bsem{b}^A(P)$ holds after the execution.

  \item If executing $C_1$ from state $P$ leads to state $Q$, and executing
    $C_2$ from state $Q$ leads to state $R$, then executing $C_1$ followed by
    $C_2$ from state $P$ leads to state $R$.

  \item If executing either $C_1$ or $C_2$ from state $P$ leads to state $Q$,
    then executing the nondeterministic choice $C_1 + C_2$ from state $P$ also
    leads to state $Q$.

  \item If executing command $C$ from state $P$ leads back to state $P$, then
    executing $C$ repeatedly (zero or more times) from state $P$ also leads
    back to state $P$.

  \item If $P$ is stronger than $P'$ and $Q'$ is stronger than $Q$, then we can
    derive $\atriple{P}{C}{Q}$ from $\atriple{P'}{C}{Q'}$.
\end{itemize}

The proofsystem is nonother than Definition \ref{def:hoaretules},
where the assertion are replaced by elements of the complete lattice $A$.

Note that we denote Abstract Hoare Triples as defined in Definition \ref{def:aht}
with the notation $\atriple{P}{C}{Q}$ while we denote the triples obtained
with the inference rules of Definition \ref{def:ahtrules} by $\vdash 
\atriple{P}{C}{Q}$.

The proofsystem for Abstract Hoare logic is sound, as the original Hoare logic.

\begin{theorem}[Soundness]
  \label{thm:atriple-sound}
  $$\vdash \atriple{P}{C}{Q} \implies \models \atriple{P}{C}{Q}$$
\end{theorem}
\begin{proof}
  By structural induction on the last rule applied in the derivation of
  $\vdash \atriple{P}{C}{Q}$:
  \begin{itemize}

    \item $(\sskip)$:
      Then the last step in the derivation was: 
      \begin{prooftree}
        \AxiomC{$ $}
        \RightLabel{$(\sskip)$}
        \UnaryInfC{$\vdash 
          \atriple{P}{\sskip}{P}$}
      \end{prooftree}

      The triple is valid since:
      \begin{align*}
        \asem{\sskip}(P)
          &= P 
          &\text{[By definition of $\asem{\cdot}$]}
      \end{align*}

      \item $(b)$:
        Then the last step in the derivation was:
        \begin{prooftree}
          \AxiomC{$ $}
          \RightLabel{$(b)$}
          \UnaryInfC{$\vdash 
          \atriple{P}{b}{\bsem{b}^A(P)}$}
        \end{prooftree}

        The triple is valid since:
        \begin{align*}
          \asem{b}(P)
            &= \bsem{b}^A(P)
            & \text{[By definition of $\asem{\cdot}$]}
        \end{align*}

      \item $(\fcmp)$: Then the last step in the derivation was:
        \begin{prooftree}
          \AxiomC{$\vdash \atriple{P}{C_1}{Q}$}
          \AxiomC{$\vdash \atriple{Q}{C_2}{R}$}
          \RightLabel{$(\mathbb{\fcmp})$}
          \BinaryInfC{$\vdash \atriple{P}{C_1 \fcmp C_2}
            {R}$}
        \end{prooftree}
          
        By inductive hypothesis:
        $\asem{C_1}(P) \leq_A Q$ and
        $\asem{C_2}(Q) \leq_A R$.

        The triple is valid since:
        \begin{align*}
          \asem{C_1 \fcmp C_2}(P)
            &= \asem{C_2}(\asem{C_1}(P))
            &\text{[By definition of $\asem{\cdot}$]} \\
            &\leq_A \asem{C_2}(Q)
            &\text{[By monotonicity of $\asem{\cdot}$]} \\
            &\leq_A R
        \end{align*}

      \item $(+)$: Then the last step in the derivation was:
        \begin{prooftree}
          \AxiomC{$\vdash \atriple{P}{C_1}{Q}$}
          \AxiomC{$\vdash \atriple{P}{C_2}{Q}$}
          \RightLabel{$(+)$}
          \BinaryInfC{$\vdash \atriple{P}{C_1 + C_2}{Q}$}
        \end{prooftree}

        By inductive hypothesis: $\asem{C_1}(P) \leq Q$ and
        $\asem{C_2}(P) \leq Q$.

        The triple is valid since:
        \begin{align*}
          \asem{C_1 + C_2}(P)
            &= \asem{C_1}(P) \join_A \asem{C_2}(P)
            &\text{[By definition of $\asem{\cdot}$]} \\
            &\leq_A Q \join_A Q \\
            &= Q
        \end{align*}

      \item $(\fix)$:
        Then the last step in the derivation was:
        \begin{prooftree}
          \AxiomC{$\vdash \atriple{P}{C}{P}$}
          \RightLabel{$(\fix)$}
          \UnaryInfC{$\vdash \atriple{P}{C ^ \fix}{P}$}
        \end{prooftree}

        By inductive hypothesis: $\asem{C}P \leq P$

        \begin{align*}
          \asem{C^\fix}(P)
            &= \lfp(\lambda P' \to P \join_A \asem{C}(P')) \\
        \end{align*}

        We will show that $P$ is a fixpoint of 
        $\lambda P' \to P \join_A \asem{C}(P')$.

        \begin{align*}
          (\lambda P' \to P \join_A \asem{C}(P'))(P)
            &= P \join_A \asem{C}(P)
            & \text{[since $\asem{C}(P) \leq P$]} \\
            &= P
        \end{align*}

        Hence $P$ is a fixpoint of $\lambda P' \to P \join_A \asem{C}(P')$,
        therefore it is above the least one, $\lfp(\lambda P' \to P 
        \join_A \asem{C}(P')) \leq_A P$ thus making the triple valid.

      \item $(\leq)$: Then the last step in the derivation was:
        \begin{prooftree}
          \AxiomC{$P \leq P'$}
          \AxiomC{$\vdash \atriple{P'}{C}{Q'}$}
          \AxiomC{$Q' \leq Q$}
          \RightLabel{$(\leq)$}
          \TrinaryInfC{$\vdash \atriple{P}{C}{Q}$}
        \end{prooftree}

        By inductive hypothesis: $\asem{C}(P') \leq_A Q'$.
        
        The triple is valid since:
        \begin{align*}
          \asem{C}(P)
            & \asem{C}(P')
            & \text{[By monotonicity of $\asem{\cdot}$]}\\
            & \leq_A Q' 
            & \text{[By inductive hypothesis]} \\
            & \leq_A Q
        \end{align*}
  \end{itemize}
\end{proof}

The proof system turns out to be relatively complete as well, in the sense that
the axioms are complete relative to what we can prove in the underlying
assertion language, that in our case is described by the complete lattice.

We will first prove a slightly weaker result, where we will show that we can
prove the strongest post-condition of every program.

\begin{theorem}[Relative $\asem{\cdot}$-completeness]
  \label{thm:post-completeness}
  $$\vdash \atriple{P}{C}{\asem{C}(P)}$$
\end{theorem}
\begin{proof}
  By structural induction on $C$:
  \begin{itemize}

    \item $\sskip$:
      By definition $\asem{\sskip}(P) = P$
      \begin{prooftree}
        \AxiomC{$ $}
        \RightLabel{$(\sskip)$}
        \UnaryInfC{$\vdash \atriple{P}{\sskip}{P}$}
      \end{prooftree}

      \item $b$:
        By definition $\asem{b}(P) = \bsem{b}^A(P)$
        \begin{prooftree}
          \AxiomC{$ $}
          \RightLabel{$(b)$}
          \UnaryInfC{$\vdash \atriple{P}{b}{\bsem{b}^A(P)}$}
        \end{prooftree}

      \item $C_1 \fcmp C_2$:
        By definition $\asem{C_1 \fcmp C_2}(P) = 
        \asem{C_2}(\asem{C_1}(P))$

        \begin{prooftree}
          \AxiomC{(Inductive hypothesis)}
          \noLine
          \UnaryInfC{$\vdash \atriple{P}{C_1}{\asem{C_1}(P)}$}
          \AxiomC{(Inductive hypothesis)}
          \noLine
          \UnaryInfC{$\vdash \atriple{\asem{C_1}(P)}{C_2}
            {\asem{C_2}(\asem{C_1}(P))}$}
          \RightLabel{$(\fcmp)$}
          \BinaryInfC{$\vdash \atriple{P}{C_1 \fcmp C_2}
            {\asem{C_2}(\asem{C_1}(P))}$}
        \end{prooftree}


      \item $C_1 + C_2$:
        By definition $\bsem{C_1 + C_2}(P) = 
        \bsem{C_1}(P) \join_A \bsem{C_2}(P)$

        \begin{prooftree}
          \AxiomC{$\pi_1$}
          \AxiomC{$\pi_2$}
          \RightLabel{$(+)$}
          \BinaryInfC{$\vdash \atriple{P}{C_1 + C_2}
            {\asem{C_1}(P) \join_A \asem{C_2}(P)}$}
        \end{prooftree}

        Where $\pi_1$:
        \begin{prooftree}
          \AxiomC{$P \leq_A P$}
          \AxiomC{(Inductive hypothesis)}
          \noLine
          \UnaryInfC{$\vdash \atriple{P}{C_1}{\asem{C_1}(P)}$}
          \AxiomC{$\asem{C_1}(P) \leq_A \asem{C_1}(P) \join_A \asem{C_2}(P)$}
          \RightLabel{$(\leq)$}
          \TrinaryInfC{$\vdash \atriple{P}{C_1}
            {\asem{C_1}(P) \join_A \asem{C_2}(P)}$}
        \end{prooftree}

        and $\pi_2$:
        \begin{prooftree}
          \AxiomC{$P \leq_A P$}
          \AxiomC{(Inductive hypothesis)}
          \noLine
          \UnaryInfC{$\vdash \atriple{P}{C_2}{\asem{C_2}(P)}$}
          \AxiomC{$\asem{C_2}(P) \leq_A \asem{C_1}(P) \join_A \asem{C_2}(P)$}
          \RightLabel{$(\leq)$}
          \TrinaryInfC{$\vdash \atriple{P}{C_2}
            {\asem{C_1}(P) \join_A \asem{C_2}(P)}$}
        \end{prooftree}

      \item $C^\fix$:
        By definition $\bsem{C^\fix}(P) = lfp(\lambda P' \to P \join_A
        \asem{C}(P')$.

        Let $K \defeq lfp(\lambda P' \to P \join_A \asem{C}(P')$
        hence $K = P \join_A \asem{C}(K)$ since it is a fixpoint, thus
        \begin{itemize}
          \item $\alpha_1$: $K \geq_A P$
          \item $\alpha_2$: $K \geq_A \asem{C}(K)$
        \end{itemize}

          \begin{prooftree}
            \AxiomC{$\alpha_1$}
            \AxiomC{$K \leq_A K$}
            \AxiomC{(Inductive hypothesis)}
            \noLine
            \UnaryInfC{$\vdash \atriple{K}{C}{\asem{C}(K)}$}
            \AxiomC{$\alpha_2$}
            \TrinaryInfC{$\vdash \atriple{K}{C}{K}$}
            \RightLabel{$(\fix)$}
            \UnaryInfC{$\vdash \atriple{K}{C^\fix}{K}$}
            \AxiomC{$K \leq_A K$}
            \RightLabel{$(\leq)$}
            \TrinaryInfC{$\vdash \atriple{P}{C^\fix}{K}$}
          \end{prooftree}
  \end{itemize}
\end{proof}

We can now show the relative completeness, by applying the rule $(\leq)$ to
achieve the desired post-condition.

\begin{theorem}[Relative completeness]
  \label{thm:completeness}
  $$\models \atriple{P}{C}{Q} \implies \vdash \atriple{P}{C}{Q}$$
\end{theorem}
\begin{proof}
  By definition of $\models \atriple{P}{C}{Q} \iff Q \geq_A \asem{C}(P)$

  \begin{prooftree}
    \AxiomC{$P \leq_A P$}
    \AxiomC{(By Theorem \ref{thm:post-completeness})}
    \noLine
    \UnaryInfC{$\vdash \atriple{P}{C}{\asem{C}(P)}$}
    \AxiomC{$Q \geq_A \asem{C}(P)$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple{P}{C}{Q}$}
  \end{prooftree}
\end{proof}

\chapter{Instantiating Abstract Hoare Logic}

In this chapter, we will demonstrate how to instantiate abstract Hoare logic to
systematically design novel program logics. We will also show that our 
abstract Hoare logic framework is sufficiently general to reason about properties that
cannot be expressed in standard Hoare logic, notably hyperproperties.

\section{Hoare logic}
\label{chp:inst-hoare}

According to Observation \ref{obs:post}, the abstract inductive semantics, when 
using $(\pow{\states}, \subseteq)$ as domain and 
$\bsem{b}^{\pow{\states}}(P) = \{ \bsem{b}(\sigma) \; \mid \sigma 
\in P \mand \bsem{b}(\sigma) \downarrow\}$ as semantics of basic commands, turns out to be equivalent to the denotational 
semantics given in Definition \ref{def:deno}. Therefore Abstract Hoare logic
(Definition \ref{def:aht}) in this instance coincides with Hoare logic (Definition
\ref{def:hoare}). Hence we obtain soundness and relative completeness for Hoare
logic directly form Theorems \ref{thm:atriple-sound} and \ref{thm:completeness}.

\subsection{Algebraic Hoare Logic}

As discussed in Section \ref{chp:intro-ahorare}, Abstract Hoare Logic was
inspired by Algebraic Hoare Logic \cite{Cousot12}. Both logics can be used to
prove properties in computer-representable abstract domains.

\begin{definition}[Algebraic Hoare triple]
  Given two Galois insertions $\langle \pow{\states}, \subseteq \rangle
  \galoiS{\alpha_1}{\gamma_1} \langle A, \leq \rangle$ and $\langle
  \pow{\states}, \subseteq \rangle \galoiS{\alpha_2}{\gamma_2} \langle B,
  \sqsubseteq \rangle$, an Algebraic Hoare triple, denoted by $\ctriple{P}{C}{Q}$, is
  valid if and only if the Hoare triple $\htriple{\gamma_1(P)}{C}{\gamma_2(Q)}$ is valid, namely:
  \begin{align*}
  \models \ctriple{P}{C}{Q} \iff \models \htriple{\gamma_1(P)}{C}{\gamma_2(Q)}
  \tag*{\qed}
  \end{align*}
\end{definition}

In the definition above,  Algebraic Hoare Logic is strongly related to
standard Hoare Logic, and, therefore, to the strongest postcondition of the program in
the concrete domain.

\begin{definition}[Algebraic Hoare logic proof system\footnote{Rules
  $(\overline{\join})$ and $(\overline{\meet})$ in \cite{Cousot12} are missing but will be
  discussed in Section \ref{chp:join-meet-rules}}]$\;$\\
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(\overline{\bot})$}
    \UnaryInfC{$\vdash \ctriple{\bot_1}{C}{Q}$}
  \end{prooftree}

  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(\overline{\top})$}
    \UnaryInfC{$\vdash \ctriple{P}{C}{\top_2}$}
  \end{prooftree}
  
  \begin{prooftree}
    \AxiomC{$\models \htriple{\gamma_1(P)}{C}{\gamma_2(Q)}$}
    \RightLabel{$(\overline{S})$}
    \UnaryInfC{$\vdash \ctriple{P}{C}{Q}$}
  \end{prooftree}
  
  \begin{prooftree}
    \AxiomC{$P \leq P'$}
    \AxiomC{$\vdash \ctriple{P'}{C}{Q'}$}
    \AxiomC{$Q' \sqsubseteq Q$}
    \RightLabel{$(\overline{\Rightarrow})$}
    \TrinaryInfC{$\vdash \ctriple{P}{C}{Q}$}
  \end{prooftree}
\end{definition}

This proof system highlights that a crucial part of the proof relies on rule
$(\overline{S})$, which embeds Hoare triples in Algebraic Hoare triples. One can
easily prove that the proof system is relatively complete by leveraging the relative
completeness of Hoare logic. In particular, only the  rule $(\overline{S})$ is
actually needed since all the implications in the abstract must also hold in
the concrete.

\subsection{Abstract Interval Logic}

By recalling Definition \ref{def:aisgi} and the properties of Galois insertions, we can easily derive a similar family of triples as those in Algebraic Hoare Logic, when  pre- and post-conditions range in the same
abstract domain.

\begin{example}[Interval logic]
  \label{exmp:int-logic}
  Applying Definition \ref{def:aisgi} to the Galois insertion on the interval
  domain defined in Example \ref{exmp:interval}, we systematically obtain a sound and
  relatively complete logic to reason about properties of programs that are
  expressible as intervals.
\end{example}

\begin{example}[Derivation in interval logic]
  \label{exmp:int-deriv}
  Let us consider the following program:
  \begin{align*}
  C \defeq ((x := 1) + (x := 3)) \fcmp ((x = 2? \fcmp x := 5) + (x \neq 2?
  \fcmp x := x - 1))\, .
  \end{align*}

\noindent
  Then the following derivation is valid:

  \begin{prooftree}
    \AxiomC{$\pi_1$}
    \AxiomC{$\pi_3$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{\top}{C}{[0, 5]}$}
  \end{prooftree}

  $\pi_1$:
  \begin{prooftree}
    \AxiomC{$\top \leq \top$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{\top}{x := 1}{[1, 1]}$}
    \AxiomC{$[1, 1] \leq [1, 3]$}
    \TrinaryInfC{$\vdash \atriple[\mathit{Int}]{\top}{x := 1}{[1, 3]}$}
    \AxiomC{$\pi_2$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{\top}{(x := 1) + (x := 3)}{[1, 3]}$}
  \end{prooftree}

  $\pi_2$:
  \begin{prooftree}
    \AxiomC{$\top \leq \top$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{\top}{x := 3}{[3, 3]}$}
    \AxiomC{$[3, 3] \leq [1, 3]$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple[\mathit{Int}]{\top}{x := 3}{[1, 3]}$}
  \end{prooftree}

  $\pi_3$:
  \begin{prooftree}
    \AxiomC{$\pi_4$}
    \AxiomC{$\pi_5$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{(x = 2? \fcmp x := 5) + (x \neq 2?
      \fcmp x := x - 1)}{[0, 5]}$}
  \end{prooftree}

  $\pi_4$:
  \begin{prooftree}
    \AxiomC{$[1, 3] \leq [1, 3]$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x = 2?}{[2]}$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[2]}{x := 5}{[5]}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x = 2? \fcmp x := 5}{[5]}$}
    \AxiomC{$[5, 5] \leq [0, 5]$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x = 2? \fcmp x := 5}{[0, 5]}$}
  \end{prooftree}
  
  $\pi_5$:
  \begin{prooftree}
    \AxiomC{$[1, 3] \leq [1, 3]$}
    \AxiomC{$\pi_6$}
    \AxiomC{$[0, 2] \leq [0, 5]$}
    \TrinaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x \neq 2? \fcmp x := x - 1}{[0,
      5]}$}
  \end{prooftree}

  $\pi_6:$
  \begin{prooftree}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x \neq 2?}{[1, 3]}$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x := x - 1}{[0, 2]}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[1, 3]}{x \neq 2? \fcmp x := x - 1}{[0,
      2]}$}
  \end{prooftree}

  The abstract post-condition $[0,5]$ is the best possible in the interval abstraction, because 
  $\asem[\mathit{Int}]{C}(\top) = [0, 5]$ holds.
\end{example}

\subsubsection{3.2.2.1 Applications}

This framework, analogously to Algebraic Hoare Logic, can be used to specify how a static
analyzer for a given abstract domain should work. Since $\asem{\cdot}$ is the
best \emph{inductive} abstract analyzer on the abstract domain $A$, and 
the whole proof system is defined in the abstract domain $A$, we can check
that a derivation is indeed correct algorithmically, as long as we assume that 
implications and basic commands can be algorithmically checked. These are usually the standard requirements
for an abstract domain to be useful in practice, that is, subject 
of an implementation. The same does not hold for Algebraic Hoare
Logic, since deciding the validity of arbitrary triples would require deciding
the validity of standard Hoare logic triples, and, in general, of course we cannot decide
implications between arbitrary properties.

\subsection{Abstract vs Algebraic Hoare Logic}

Clearly, Algebraic Hoare Logic can derive the same triples that are derivable
by Abstract Hoare Logic when instantiated through a Galois insertion from
$\pow{\states}$ as we did in Example \ref{exmp:int-logic}. From Theorem~\ref{thm:sound-ai}, 
it turns out that $\asem{\cdot}$ is a sound overapproximation of
$\sem{\cdot}$.

\begin{theorem}[Abstract entails Algebraic] \label{th:AeA}
  $\vdash \atriple{P}{C}{Q} \implies \vdash \ctriple{P}{C}{Q}$
\end{theorem}
\begin{proof}
  \begin{align*}
    \vdash \atriple{P}{C}{Q}
      &\implies \asem{C}(P) \leq Q
      &\text{[From Theorem \ref{thm:atriple-sound}]} \\
      &\implies \sem{C}(\gamma(P)) \subseteq \gamma(Q)
      &\text{[From Theorem \ref{thm:sound-ai}]} \\
      &\implies \vdash \htriple{\gamma(P)}{C}{\gamma(Q)}
      &\text{[From Theorem \ref{thm:hlogic-complete}]} \\
      &\implies \vdash \ctriple{P}{C}{Q}
      &\text{[From rule $(\overline{S})$]} \tag*{\qedhere}
  \end{align*}
\end{proof}

However, the converse of Theorem~\ref{th:AeA} does not hold. The relative completeness of Algebraic Hoare
Logic is stated with respect to the best correct approximation of $\sem{\cdot}$, differently from 
Abstract Hoare Logic which considers $\asem{\cdot}$.

\begin{example}[Counterexample to the converse of Theorem~\ref{th:AeA}]
  From Example \ref{exmp:int-deriv}, we know that $\vdash \atriple{\top}{C}{[0, 5]}$ is
  the best Abstract Hoare triple that we can derive. However, we have that $\sem{C}{\top} = \{0,
  2\}$. By Theorem \ref{thm:hlogic-complete}, we can infer
  $\vdash \htriple{\top}{C}{\{0, 2\}}$. Hence, by rule $(\overline{S})$, we can
  obtain $\vdash \ctriple{\top}{C}{[0, 2]}$, which cannot be derived in Abstract Hoare
  Logic.
\end{example}

This divergence  between abstract and 
algebraic Hoare logics arises because, through the rule $(S)$ rule of Algebraic Hoare logic,
we are always able to prove the best correct approximation of any program $C$. However, the 
property of being a best correct approximation is not compositional, 
meaning that the function composition of two best correct approximations is not
the best correct approximation of the composition of these functions. Since in the
abstract semantics the program composition is done in ``the abstract'', it is
impossible to expect to be able to derive any possible best correct
approximation, except in trivial abstract domains such as the concrete domain
$\pow{\states}$ or the  one-element abstraction $\{\top\}$.

\section{Hoare logic for hyperproperties}

\renewcommand{\chi}{\mathbb{X}}

\subsection{Introduction to Hyperproperties} \label{chp:hyper}

Program hyperproperties \cite{Clarkson08} extend traditional program
properties by considering relationships between multiple executions of a
program, rather than focusing on individual traces. This concept is essential
for reasoning about security and correctness properties that involve
comparing different executions, such as non-interference and information
flow security \cite{Gougen82}.

Standard program properties, such as those of Hoare logic, range into the set
$\pow{\states}$. By contrast, hyperproperties range in $\pow{\pow{\states}}$,
as they encode relations between different executions. A typical  example is the
property of a program of being deterministic. For instance, if our programs involve a
single integer variable \(x\), proving determinism involves an infinite number
of Hoare triples of the form: for each \(n \in \mathbb{N}\), there exists \(m
\in \mathbb{N}\) such that $\models \htriple{\{ x = n \}}{C}{\{ x = m \}}$ holds.
However, determinism can be succinctly encoded by a single hyper triple as follows:
\begin{align*}
\models \htriple{\{ P \in \pow{\pow{\states}} \mid |P| = 1 \}}{C}{\{ Q \in
\pow{\pow{\states}} \mid |Q| = 1 \}}\, .
\end{align*}

\begin{definition}[Strongest Hyper Postcondition] \label{def:shp}
  The strongest postcondition of a program \(C\) starting from a collection of 
  sets of states \(\chi \in \pow{\pow{\states}}\) is defined as follows: 
  \begin{equation*}
  \{ \sem{C}(P) \mid P 
  \in \chi \}\, . \tag*{\qed}
  \end{equation*}
\end{definition}

Note that Definition~\ref{def:shp} is justified by the requirement that 
we are interested in modeling the strongest postcondition of every initial state ranging in
$\chi$.

\subsection{Inductive Definition of the Strongest Hyper Postcondition}

To design a sound and relatively complete logic for hyperproperties within
our framework, it is crucial to define an abstract inductive semantics that
precisely computes the strongest hyper postcondition. This objective has been
investigated in prior works \cite{Mounir17, Mastroeni18}, mostly in an 
abstract interpretation-based scenario. However, existing approaches often provide an
over-approximation of the strongest hyper postcondition, which, while suitable
for abstract interpretation, falls short of maintaining relative completeness
in our context.

In \cite{Mounir17}, for instance, the hyper semantics of the branching command 
$\mathbf{if} \; b \; \mathbf{then} \; C_1 \; \mathbf{else} \; C_2$ from 
a starting hyper-state $\mathbb{T}$ is defined to be $\{ \sem{b ? \fcmp C_1} T
\cup \sem{\neg b ? \fcmp C_2} \mid T \in \mathbb{T}\}$, thereby lacking
inductiveness. It is worth remarking that with this noninductive definition, we have that, 
for any program $C$,
the hypersemantics of  
$\mathbf{if} \; 1 = 1 \; \mathbf{then} \; C$ coincides with that of $C$, thus making this
hyper semantics practically meaningless for program analysis.

The fundamental issue lies in the fact that in the domain $\pow{\pow{\states}}$, ordered w.r.t.\ 
the usual subset inclusion, the least upper bound, namely set union, fails to distinguish between different
executions, as shown by the following example.

\begin{example}
  \label{exmp:determinism}
  Let $\mathcal{X} \defeq \{\{1, 2, 3\}, \{5\}\}$. Clearly, we have that:
  $$\asem[\pow{\pow{\states}}]{(x := x + 1) + (x := x + 2)}(\mathcal{X}) = 
  \{\{2, 3, 4\}, \{6\}, \{3, 4, 5\}, \{7\}\},$$
  which is obviously different from the strongest hyper postcondition 
  $\{\{2, 3, 4, 5\}, \{6, 7\}\}$.
\end{example}

When applying the rule for non-deterministic choice,
\begin{align*}
\asem[\pow{\pow{\states}}]{C_1 + C_2}(\mathcal{P}) =
\asem[\pow{\pow{\states}}]{C_1}(\mathcal{P}) \;\cup\;
\asem[\pow{\pow{\states}}]{C_2}(\mathcal{P})\, ,
\end{align*}
the union of outermost sets is
considered rather than of the innermost sets that include actual executions. Attempts to
alter the ordering on the domain $\pow{\pow{\states}}$ turned out to be unsuccessful 
as each set lacks information about the generating execution, thus leading to an unavoidable loss
of precision in the definition of the union. 

To the best of our knowledge, no approach has been put forward for defining 
an abstract inductive semantics that exactly
computes the strongest hyper postcondition. Existing works just provide sound
overapproximations, which are adequate for abstract interpreters, but are not 
precise enough for verifying certain hyperproperties within
Abstract Hoare logic, especially where precision in abstract inductive
semantics is compromised.


\subsection{Hyper Domains}

To address the limitations of $\pow{\pow{\states}}$ discussed above, we introduce a 
family of domains designed to keep track of the execution of
interest across different executions. Our definition leverages an index set $K$ ($K$ stands for ``keys'') 
to enumerate
individual executions, and, accordingly, define the join operation in a manner that allows us
to distinguish them. 

\begin{definition}[Hyper Domain]\label{def:hd}
  Given a complete lattice $B$ and a set $K$, the hyper domain $H(B)_K$ is
  defined as follows: $$H(B)_K \defeq K \to B + \textit{undef}\, .$$

\noindent
  The structure of complete lattice of $H(B)_K$ is defined  by lifting the
  pointwise lattice of $B + \text{undef}$, where $B + \text{undef}$ forms a
  complete lattice on $B$ where \textit{undef} is the new bottom element,
  meaning that $\textit{undef} \: \mathrel{<} \bot_B$ (see Figure~\ref{fig:hd}). \qed
\end{definition}

\begin{figure}[t]\label{fig:hd}
\begin{center}
\begin{tikzpicture}
  \node [] (a) at (0, -1) {};
  \node [] (0) at (0, 0) {$\bot$};

  \node [] (1) at (-1, 1) {};
  \draw (0) to (1);
  \node [] (2) at (0, 1) {};
  \draw (0) to (2);
  \node [] (3) at (+1, 1) {};
  \draw (0) to (3);
  
  \node [] (4) at (-1, 2) {};
  \node [] (5) at (0, 2) {};
  \node [] (6) at (+1, 2) {};

  \node [] (u) at (0, 1.5) {$\dots$};
  
  \node [] (7) at (0, 3) {$\top$};
  \draw (6) to (7);
  \draw (5) to (7);
  \draw (4) to (7);
\end{tikzpicture}
\qquad
\qquad
\qquad
\begin{tikzpicture}
  \node [] (a) at (0, -1) {$\textit{undef}$};
  \draw (a) to (0);
  \node [] (0) at (0, 0) {$\bot$};

  \node [] (1) at (-1, 1) {};
  \draw (0) to (1);
  \node [] (2) at (0, 1) {};
  \draw (0) to (2);
  \node [] (3) at (+1, 1) {};
  \draw (0) to (3);
  
  \node [] (4) at (-1, 2) {};
  \node [] (5) at (0, 2) {};
  \node [] (6) at (+1, 2) {};

  \node [] (u) at (0, 1.5) {$\dots$};
  
  \node [] (7) at (0, 3) {$\top$};
  \draw (6) to (7);
  \draw (5) to (7);
  \draw (4) to (7);
\end{tikzpicture}
\end{center}
\caption{On the left the Hasse diagram of $B$, on the right the Hasse diagram of
$B + undef$}
\end{figure}
 
Let us point out that the role played by the index set 
$K$ in Definition~\ref{def:hd} is merely that of encoding different executions, where no specific
requirements on its elements are assumed, while $K$ should simply have enough distinct indices to account
for all the executions of interest. 

\begin{definition}[Hyper Instantiation]
  Given an instantiation of the abstract inductive semantics on the domain $B$ with
  semantics for basic commands $\bsem{\cdot}^B$, the abstract inductive
  semantics for the hyper domain $H(B)_K$ is accordingly defined bu taking
  as semantics of the base commands:

  $$\bsem{b}^{H(B)_K}(\chi) \defeq \lambda r . \bsem{b}^B(\chi(r))\, .$$
\end{definition}

Hence, this notion of hyper instantiation lifts the abstract inductive semantics from
the domain $B$ to its ``hype'' version, by applying the semantics of basic commands
from $B$ to each execution.
Next, we show that the abstract inductive semantics instantiated on a
hyper-domain preserves non-interference, meaning that the hyper
inductive semantics yields the same results as computing the original semantics
on each execution.

\begin{theorem}[Non-interference between executions]
    \label{thm:hyper-add} For all programs $C$, we have that
    $$\asem[H(B)_K]{C}(\mathcal{\chi}) = \lambda r . \asem[B]{C}(\chi(r))\, .$$
\end{theorem}
\begin{proof}
  By structural induction on $C$:
  \begin{itemize}
    \item $\sskip$:
      \begin{align*}
        \asem[H(B)_K]{\sskip}(\chi) 
          &= \chi
          &\text{[By definition of $\asem[H(B)_K]{\cdot}$]} \\
          &= \lambda r . \chi(r) 
          &\text{[By extensionality]}\\
          &= \lambda r . \asem[B]{\sskip}(\chi(r))
          &\text{[By definition of $\asem[B]{\cdot}$]} \\
      \end{align*}

    \item $b$:
      \begin{align*}
        \asem[H(B)_K]{b}(\chi) 
          &= \lambda r . \asem[B]{b}(\chi(r))
      \end{align*}

    \item $C_1 \fcmp C_2$:
      \begin{align*}
        \asem[H(B)_K]{C_1 \fcmp C_2}(\chi) 
          &= \asem[H(B)_K]{C_2}(\asem[H(B)_K]{C_1}(\chi))
          &\text{[By definition of $\asem[H(B)_K]{\cdot}$]} \\
          &= \asem[H(B)_K]{C_2}(\lambda r_1 . \asem[B]{C_1}(\chi(r_1)))
          &\text{[By inductive hypothesis]} \\
          &= \lambda r_2 . \asem[B]{C_2}(\lambda r_1 . \asem[B]{C_1}(\chi(r_1))(r_2))
          &\text{[By inductive hypothesis]} \\
          &= \lambda r_2 . \asem[B]{C_1 \fcmp C_2}(\chi(r_2))
          &\text{[By definition of $\asem[B]{\cdot}$]} \\
      \end{align*}

    \item $C_1 + C_2$:
      \begin{align*}
        \asem[H(B)_K]{C_1 + C_2}(\chi)
          &= \asem[H(B)_K]{C_1}(\chi) \lor \asem[H(B)_K]{C_2}(\chi)
          &\text{[By definition of $\asem[H(B)_K]{\cdot}$]} \\
          &= (\lambda r_1 . \asem[B]{C_1}(\chi(r_1))) \lor (\lambda r_2 . \asem[B]{C_1}(\chi(r_2)))
          &\text{[By inductive hypothesis]} \\
          &= \lambda r . \asem[B]{C_1}(\chi(r)) \lor \asem[B]{C_2}(\chi(r)) \\
          &= \lambda r . \asem[B]{C_1 + C_2}(\chi(r))
          &\text{[By definition of $\asem[B]{\cdot}$]} \\
      \end{align*}

    \item $C^\fix$:
      \begin{align*}
        \asem[H(B)_K]{C^\fix}(\chi)
          &= \lfp(\lambda \psi . \chi \lor \asem[H(B)_K]{C}(\psi))
          &\text{[By definition of $\asem[H(B)_K]{\cdot}$]} \\
          &= \lfp(\lambda \psi . \chi \lor \lambda r . \asem[B]{C}(\psi(r)))
          &\text{[By inductive hypothesis]} \\
          &= \lambda r . \lfp(\lambda P . \chi(r) \lor \asem[B]{C} P)
          &\text{[By definition of $\asem[B]{\cdot}$]} \\
          &= \lambda r . \asem[B]{C^\fix}(\chi(r))
      \end{align*}
  \end{itemize}
\end{proof}


\subsection{Inductive Definition for Hyper Postconditions}

Our definition of hyper domains allows us to overcome the limitations of
$\pow{\pow{\states}}$ found in literature. On the other hand, we 
now use a different domain in our abstract inductive
semantics. To bridge this gap, we establish a method for converting standard
hyperproperties to their hyper domain counterparts and vice versa. This
involves defining a pair of functions, referred to as \emph{conversion pair},
to make this conversion simpler. Of course, there exist infinitely many functions
to convert a standard hyperproperty into a version using hyper domains---due to
the infinite representations of the same property---and we exploit a single
representative (which is an $1$-$1$ function) to encapsulate all these representations, 
so that
our results will remain independent of the chosen indexing function.

\begin{definition}[Conversion Pair]\label{def:cp}
  Given a $1$-$1$ function $\mathit{idx} : B \to K$, the conversion pair $\langle \alpha,\beta\rangle$ is defined
  as follows:
%
  \begin{align*}
    \alpha &\;\;:\; H(B)_K \to \pow{B} \\
    \alpha(\chi) &\defeq \{ \chi(r) \; \mid r \in K \mand \chi(r)\downarrow \} \\
    \\
    \beta &\;\;:\; \pow{B} \to H(B)_K \\
    \beta(\mathcal{X}) &\defeq \lambda r . \begin{cases}
      P              & \exists P \in \mathcal{X} \; \text{such that} \; \mathit{idx}(P) = r \\
      \textit{undef} & \text{otherwise}
    \end{cases}
  \end{align*}
\end{definition}

By instantiating the hyper domain to $H(\pow{\states})_{\mathbb{R}}$, we
show that our abstract inductive semantics actually defines  the strongest hyper
postcondition.

\begin{theorem}[Abstract Inductive Semantics as Strongest Hyper Postcondition]
  \label{thm:hyperpost} 
  $$\alpha(\asem[H(\pow{\states})_\mathbb{R}]{C}(\beta(\mathcal{X}))) = \{ \asem[\pow{\states}]{C}(P) \mid P \in \mathcal{X} \}$$
\end{theorem}
\begin{proof}
  \begin{align*}
    \alpha(\asem[H(\pow{\states})_\mathbb{R}]{C}(\beta(\mathcal{X})))
      &= \alpha(\lambda r . \asem[\pow{\states}]{C}(\beta(\mathcal{X})(r)))
      &\text{[By Theorem \ref{thm:hyper-add}]} \\
      &= \{ \asem[\pow{\states}]{C}(\beta(\mathcal{X})(r))\downarrow \;
        \mid r \in \mathbb{R} \}
      &\text{[By the definition of $\alpha$]}\\
      &= \{ \asem[\pow{\states}]{C}(P) \mid P \in \mathcal{X} \}
      &\text{[By the definition of $\beta$ and injectivity]}
  \end{align*}
\end{proof}

\subsection{Hyper Hoare Triples}

The instantiation of hyper domains provides a sound and complete Hoare-like
logic for hyperproperties, particularly when using the function $\alpha$ of Definition~\ref{def:cp} on pre- and
postconditions.

\begin{example}[Determinism in Abstract Hoare Logic]
  As discussed in Example \ref{exmp:determinism}, we express the determinism,
  up to termination, of a command by proving that the hyperproperty $\{P \mid
  |P| = 1\}$ serves as both precondition and postcondition for the command.

  We assume that the language $\lang$ uses single-variable assignments only, so that 
  program states are represented simply by integers.

  The property $\mathbb{P}$ we use as precondition is defined as follows:
  $$\mathbb{P} \defeq \lambda r . \begin{cases}
    \{ x \} & \exists x \in \states \; \text{such that} \; \mathit{idx}(P) = r \\
    \textit{undef} & \text{otherwise}
  \end{cases}$$

  We prove that $\sskip$ (i.e., the skip command) is deterministic:
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(\sskip)$}
    \UnaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {\sskip}{\mathbb P}$}
  \end{prooftree}

  Since $\alpha(\mathbb P) = \{\ldots, \{-1\}, \{0\}, \{1\}, \ldots\}$, we can therefore infer 
  that the command is deterministic.

  Similarly, we can prove that the increment function is deterministic as follows:
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(:=)$}
    \UnaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {x := x + 1}{\mathbb Q}$}
  \end{prooftree}
  %
  where $\mathbb Q  \defeq \lambda r . \begin{cases}
    \{ x + 1\} & \exists \{x\} \in \pow{\states} \; \text{such that} \; \mathit{idx}(P) = r \\
    \textit{undef} & \text{otherwise}
  \end{cases}$
%
  Clearly, we have that $\alpha(\mathbb Q) = \{..., \{0\}, \{1\}, \{2\}, ...\}$, thus proving
  determinism.

  Finally, we can establish that a nondeterministic choice between two identical
  programs remains deterministic by the following proof:
  \begin{prooftree}
    \AxiomC{$ $}
    \RightLabel{$(:=)$}
    \UnaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {x := x + 1}{\mathbb Q}$}
    \AxiomC{$ $}
    \RightLabel{$(:=)$}
    \UnaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {x := x + 1}{\mathbb Q}$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {(x := x + 1) + (x := x + 1)}{\mathbb Q}$}
  \end{prooftree}
%
  However, different programs cannot be handled in the same way:
  \begin{prooftree}
    \AxiomC{$\mathbb P \leq \mathbb P$}
    \AxiomC{$ $}
    \RightLabel{$(\sskip)$}
    \UnaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {\sskip}{\mathbb P}$}
    \AxiomC{$\mathbb P \leq \mathbb P \lor \mathbb Q$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {\sskip}{\mathbb P \lor \mathbb Q}$}
    \AxiomC{$\pi$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {\sskip + (x := x + 1)}{\mathbb P \lor \mathbb Q}$}
  \end{prooftree}
  where the proof tree $\pi$ is the following:
  \begin{prooftree}
    \AxiomC{$\mathbb P \leq \mathbb P$}
    \AxiomC{$ $}
    \RightLabel{$(:=)$}
    \UnaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {x := x + 1}{\mathbb Q}$}
    \AxiomC{$\mathbb Q \leq \mathbb P \lor \mathbb Q$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple[H(\pow{\states})_\mathbb{R}]{\mathbb P}
      {x := x + 1}{\mathbb P \lor \mathbb Q}$}
  \end{prooftree}
%
  Clearly, we have that $\alpha(\mathbb P \lor \mathbb Q) = 
  \{..., \{-1, 0\}, \{0, 1\}, \{1, 2\}, ...\}$. 
   Let us observe that different elements within the hyper domain may correspond to the same
  hyperproperty, therefore reflecting that the nondeterministic choice does not always
  ``preserve'' hyperproperties. This approach parallels other logics that handle
  hyperproperties by introducing a new disjunction operator capable of
  distinguishing between different executions. \qed
\end{example}


Hyper Hoare Logic \cite{Darnier2023} is a related Hoare-like logic that provides a
sound and relatively complete program logic for hyperproperties. While Hyper Hoare Logic was
specifically designed for this purpose, it turns out to be equivalent to the logic derived
from our abstract Hoare logic framework. Notably, it departs from using the
classical disjunction connective---equivalent to the least upper bound in
$\pow{\pow{\states}}$---adopting instead a peculiar disjunction operator $\otimes$ 
which is able to  distinguish different executions, similarly to the least
upper bound in our hyper domain.


\section{Partial Incorrectness}
\label{chp:partial-incorrectness}

Any instantiation of the abstract inductive semantics provides a corresponding program logic, 
as the semantics is parameterized by the complete lattice
\( A \), and the dual  \( A^{\mathrm{op}} \) of a complete lattice \( A \) is a complete lattice as well. Therefore,
we can derive the dual abstract inductive semantics on the complete lattice
\( A^{\mathrm{op}} \).

\begin{definition}[Dual Abstract Inductive Semantics]
  Given an abstract inductive semantics defined on a complete lattice \( A \)
  with basic commands \( \bsem{\cdot}^A \), the \emph{dual} abstract inductive
  semantics is defined on the complete lattice \( A^{\mathrm{op}} \) with basic command
  semantics \( \bsem{\cdot}^{A^{\mathrm{op}}} = \bsem{\cdot}^A \). \qed
\end{definition}

Since the dual abstract inductive semantics is itself an abstract inductive
semantics, it naturally induces an Abstract Hoare Logic. In the dual lattice,
where the partial order is reversed, operations such as joins and meets are
swapped, leading to an inversion of \( \lfp \) and \( \gfp \). Hence, the dual
abstract inductive semantics, as given in the dual lattice, can be formulated
as follows:
\begin{align*}
  \asem[A^{\mathrm{op}}]{\sskip}        &= id &&= id \\
  \asem[A^{\mathrm{op}}]{b}             &= \bsem{b}^{A^{\mathrm{op}}} &&= \bsem{b}^A \\
  \asem[A^{\mathrm{op}}]{C_1 \fcmp C_2} &= \asem[A^{\mathrm{op}}]{C_2} \circ \asem[A^{\mathrm{op}}]{C_1} &&= \asem[A^{\mathrm{op}}]{C_2} \circ \asem[A^{\mathrm{op}}]{C_1} \\
  \asem[A^{\mathrm{op}}]{C_1 + C_2}     &= \lambda P . \asem[A^{\mathrm{op}}]{C_1} P \join_{A^{\mathrm{op}}} \asem[A^{\mathrm{op}}]{C_2} P &&= \lambda P . \asem[A^{\mathrm{op}}]{C_1} P \meet_A \asem[A^{\mathrm{op}}]{C_2} P \\
  \asem[A^{\mathrm{op}}]{C^\fix}        &= \lambda P . \lfp_{A^{\mathrm{op}}}(\lambda P'. P \join_{A^{\mathrm{op}}} \asem[A^{\mathrm{op}}]{C} P') &&= \lambda P . \gfp_{A}(\lambda P'. P \meet_A \asem[A^{\mathrm{op}}]{C} P')
\end{align*}

In this dual abstract inductive semantics, we observe that in the
dual lattice \( A^{\mathrm{op}} \), non-deterministic choices are handled by taking the
meet of two branches, reflecting certainty rather than possibility. Instead of
considering all reachable states (i.e., union of states reached by each branch), it
considers the intersection of states guaranteed to be reached by both branches.
This inversion similarly applies to the \( \fix \) command.

Due to the reverse order in the dual lattice, the validity of Abstract Hoare
triples is accordingly changed as follows:
$$\models \atriple[A^{\mathrm{op}}]{P}{C}{Q} \iff \asem{C}(P) \leq_{A^{\mathrm{op}}} Q \iff \asem[A^{\mathrm{op}}]{C}(P) \geq_A Q\, .$$

When deriving the dual abstract inductive semantics from the abstract
inductive semantics on \( \pow{\states} \) (i.e., strongest postcondition), the dual
semantics corresponds to the strongest liberal postcondition as introduced in
\cite{Zhang22} (notably in the Boolean case). These triples are referred to as ``partial
incorrectness'' triples, entailing that if \( \models \atriple[A^{\mathrm{op}}]{Q}{C}{P} \), then
\( P \) over-approximates the states reaching \( Q \), accounting for
termination. This notion aligns with the ``necessary preconditions'' investigated in
\cite{Cousot13}, where the Abstract Hoare Logic provides a sound and complete
proof system for this logic.

\chapter{Extending the proof system}

The proof system for Abstract Hoare logic given in Definition \ref{def:ahtrules} is
rather minimalistic. The overall objective of Abstract Hoare logic is to establish a
comprehensive framework for designing Hoare-like logics, aiming to require as
few assumptions as possible on both the assertion language and the semantics of
base commands. Throughout this chapter, we explore its potential to derive
additional sound rules for the proof system by introducing more constraints
either on the complete lattice of assertions or on the semantics of base commands.

\section{Merge rules}
\label{chp:join-meet-rules}

When designing a software verification tool, the capability to perform multiple 
local reasonings and, subsequently, merge their results provides clear benefits.  
An example of this arises for the conjunction rule in concurrent separation 
logic \cite{Brookes16}.

In Hoare logic, the following two merge rules turn out to be sound:

\begin{definition}[Merge rules in Hoare logic] $\;$\\
  \begin{prooftree}
    \AxiomC{$\vdash \htriple{P_1}{C}{Q_1}$}
    \AxiomC{$\vdash \htriple{P_2}{C}{Q_2}$}
    \RightLabel{$(\lor)$}
    \BinaryInfC{$\vdash \htriple{P_1 \lor P_2}{C}{Q_1 \lor Q_2}$}
  \end{prooftree}
  
  \begin{prooftree}$\;$\\
    \AxiomC{$\vdash \htriple{P_1}{C}{Q_1}$}
    \AxiomC{$\vdash \htriple{P_2}{C}{Q_2}$}
    \RightLabel{$(\land)$}
    \BinaryInfC{$\vdash \htriple{P_1 \land P_2}{C}{Q_1 \land Q_2}$}
  \end{prooftree}
\end{definition}

Although not essential for the completeness of the proof system, the practice of 
performing two distinct analyses and, subsequently, merging their results can bring 
advantages. As noted in \cite{Cousot12}, the abstract versions of merge 
rules are generally unsound in Algebraic Hoare Logic, a fact that also holds in 
Abstract Hoare logic. We will present a counterexample for the  rule $(\lor)$, 
which can be readily adapted to illustrate issues with the  rule $(\land)$.

\begin{definition}[Merge rules in Abstract Hoare logic] $\;$\\
  \begin{prooftree}
    \AxiomC{$\vdash \atriple{P_1}{C}{Q_1}$}
    \AxiomC{$\vdash \atriple{P_2}{C}{Q_2}$}
    \RightLabel{$(\lor)$}
    \BinaryInfC{$\vdash \atriple{P_1 \lor P_2}{C}{Q_1 \lor Q_2}$}
  \end{prooftree}
  
  \begin{prooftree}$\;$\\
    \AxiomC{$\vdash \atriple{P_1}{C}{Q_1}$}
    \AxiomC{$\vdash \atriple{P_2}{C}{Q_2}$}
    \RightLabel{$(\land)$}
    \BinaryInfC{$\vdash \atriple{P_1 \land P_2}{C}{Q_1 \land Q_2}$}
  \end{prooftree}
\end{definition}

\begin{example}[Counterexample for the  rule $(\lor)$]
  Let $\atriple[\mathit{Int}]{\cdot}{\cdot}{\cdot}$ be the Abstract Hoare logic 
  instantiation of Example \ref{exmp:int-logic} for the Abstract Interval Logic, and
  let $$C \defeq (x = 4? \fcmp x := 50) + (x \neq 4? \fcmp x := x + 1)\, .$$ 
  We have the following two derivations:
  \begin{prooftree}
    \AxiomC{$\pi_1$}
    \AxiomC{$\pi_2$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{C}{[4, 4]}$}
  \end{prooftree}
  where $\pi_1$ is:
  \begin{prooftree}
    \AxiomC{$[3, 3] \leq [3, 3]$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{x = 4?}{\bot}$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{\bot}{x := 50}{\bot}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{x = 4? \fcmp x := 50}{\bot}$}
    \AxiomC{$\bot \leq [4, 4]$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{x = 4? \fcmp x := 50}{[4, 4]}$}
  \end{prooftree}
  and $\pi_2$ is:
  \begin{prooftree}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{x \neq 4?}{[3, 3]}$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{x := x + 1}{[4, 4]}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{x \neq 4? \fcmp x := x + 1}{[4, 4]}$}
  \end{prooftree}

\noindent
  Moreover, we have:
  \begin{prooftree}
    \AxiomC{$\pi_3$}
    \AxiomC{$\pi_4$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{C}{[6, 6]}$}
  \end{prooftree}
%
  where $\pi_3$ is:
  \begin{prooftree}
    \AxiomC{$[5, 5] \leq [5, 5]$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{x = 4?}{\bot}$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{\bot}{x := 50}{\bot}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{x = 4? \fcmp x := 50}{\bot}$}
    \AxiomC{$\bot \leq [6, 6]$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{x = 4? \fcmp x := 50}{[6, 6]}$}
  \end{prooftree}
%
  and $\pi_4$ is:
  \begin{prooftree}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{x \neq 4?}{[6, 6]}$}
    \AxiomC{$$}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{x := x + 1}{[6, 6]}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{x \neq 4? \fcmp x := x + 1}{[6, 6]}$}
  \end{prooftree}

\noindent
  Thus we can derive the following proof tree:
  \begin{prooftree}
    \AxiomC{$\vdash \atriple[\mathit{Int}]{[5, 5]}{C}{[6, 6]}$}
    \AxiomC{$\vdash \atriple[\mathit{Int}]{[3, 3]}{C}{[4, 4]}$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[3, 5]}{C}{[4, 6]}$}
  \end{prooftree}

\noindent
   However, this is clearly unsound because:
  \begin{align*}
    \asem[\mathit{Int}]{C}([3, 5]) &= \asem[\mathit{Int}]{x = 4? \fcmp x := 50}([3, 5])
      \lor \asem[\mathit{Int}]{x \neq 4? \fcmp x := x + 1}([3, 5]) \\
                          &= \bsem{x := 50}^{\mathit{Int}}(\bsem{x = 4?}^{\mathit{Int}}([3, 5]))
      \lor \bsem{x := x + 1}^{\mathit{Int}}(\bsem{x \neq 4?}^{\mathit{Int}}([3, 5])) \\
                          &= [50, 50] \lor [4, 6] \\
                          &= [4, 50]
  \end{align*}
  %
  and we have that $[4, 50] \not \leq [4, 6]$. \qed
\end{example}

One might claim that the issue is merely ``local'', because $\gamma([3,3]) \cup 
\gamma([5,5]) = \{3, 5\} \neq \{3, 4, 5\} = \gamma([3,3] \lor [5,5])$, so that one could guess
that requiring a local disjunctive condition such as 
$\gamma(P_1 \lor P_2) = \gamma(P_1) \cup \gamma(P_2)$ could fix the unsoundness, 
since this least upper bound adds new states in the precondition. However, this 
guess turns out to be incorrect. In fact, we can construct arbitrary programs 
that exploit the 
fact that $\lor$ is, in general, a convex operation capable of introducing new elements
in its over-approximation. 

%\begin{definition}[Local rule  $\join$ for abstract Hoare logic] $\;$\\
%\end{definition}

\begin{example}[Counterexample for a local disjunctive  rule]\label{ex:cex-ldr}
Consider the following rule 
  \begin{prooftree}
    \AxiomC{$\gamma(P_1 \join P_2) = \gamma(P_1) \cup \gamma(P_2)$}
    \AxiomC{$\vdash \atriple{P_1}{C}{Q_1}$}
    \AxiomC{$\vdash \atriple{P_2}{C}{Q_2}$}
    \RightLabel{$(\join\text{-local})$}
    \TrinaryInfC{$\vdash \atriple{P_1 \lor P_2}{C}{Q_1 \lor Q_2}$}
  \end{prooftree}
%
and  let $\atriple[\mathit{Int}]{\cdot}{\cdot}{\cdot}$ be the Abstract Hoare logic 
  instantiation to Interval Logic described in Example \ref{exmp:int-logic}. Let us consider the program
  $$C \defeq (x = 0? + x = 2?) \fcmp x = 1?\, .$$

  The following derivation can be inferred:
  \begin{prooftree}
    \AxiomC{$\pi_1$}
    \AxiomC{}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[0, 0]}{x = 1?}{\bot}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[0, 1]}{C}{\bot}$}
  \end{prooftree}
%
  where $\pi_1$ is:
  \begin{prooftree}
    \AxiomC{}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[0, 1]}{x = 0?}{[0, 0]}$}
    \AxiomC{}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[0, 1]}{x = 2?}{[\bot]}$}
    \AxiomC{$\bot \leq [0, 0]$}
    \RightLabel{$(\leq)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[0, 1]}{x = 2?}{[0, 0]}$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[0, 1]}{(x = 0?) + (x = 2?)}{[0, 0]}$}
  \end{prooftree}

  Also, we have that: 
  \begin{prooftree}
    \AxiomC{$\pi_2$}
    \AxiomC{}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{x = 1?}{\bot}$}
    \RightLabel{$(\fcmp)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{C}{\bot}$}
  \end{prooftree}
  %
  where $\pi_2$ is:
  \begin{prooftree}
    \AxiomC{}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{x = 0?}{[\bot]}$}
    \AxiomC{$\bot \leq [2, 2]$}
    \RightLabel{$(\leq)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{x = 0?}{[2, 2]}$}
    \AxiomC{}
    \RightLabel{$(b)$}
    \UnaryInfC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{x = 2?}{[2, 2]}$}
    \RightLabel{$(+)$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{(x = 0?) + (x = 2?)}{[2, 2]}$}
  \end{prooftree}
  
  Thus, we have in turn the following proof tree:
  \begin{prooftree}
    \AxiomC{$\vdash \atriple[\mathit{Int}]{[2, 2]}{C}{\bot}$}
    \AxiomC{$\vdash \atriple[\mathit{Int}]{[0, 1]}{C}{\bot}$}
    \BinaryInfC{$\vdash \atriple[\mathit{Int}]{0, 2}{C}{\bot}$}
  \end{prooftree}

\noindent
  However, its conclusion is  clearly unsound because:
  \begin{align*}
    \asem[\mathit{Int}]{C}([0, 2]) &= \bsem{x = 1?}^{\mathit{Int}}(\bsem{x = 0?}^{\mathit{Int}}([0, 2]) 
      \join \bsem{x = 2}^{\mathit{Int}}([0, 2])) \\
                          &= \bsem{x = 1?}^{\mathit{Int}}([0, 0] \join [2, 2]) \\
                          &= \bsem{x = 1?}^{\mathit{Int}}([0, 2]) \\
                          &= [1, 1]
  \end{align*}
%
  and, obviously, $[1, 1] \not \leq \bot$. \qed
\end{example}

Example~\ref{ex:cex-ldr} shows the actual root cause of the issue of the rule
for disjunction, namely the overapproximation 
introduced by the abstract join $\join$, which is unrelated to the preconditions. 
More precisely, 
consider the program $$C' \defeq (x = 1? \fcmp x = 0?) + (x = 2? \fcmp x = 0?)\, ,$$
where the issue does not appear. Despite the fact that $C$ and $C'$ are equivalent
programs in the concrete domain $\pow{\pow{\states}}$, they differ in the
$\mathit{Int}$ abstract domain. Therefore, the equality $\asem{(C_1 + C_2) \fcmp C_3} =
\asem{(C_1 \fcmp C_3) + (C_2 \fcmp C_3)}$, in general, does not hold.
In particular, we can easily demonstrate that for a subset of the preconditions---namely, those admitting a program capable of having them as a postcondition---requiring the validity of
the distributivity rule is equivalent to assuming that the additivity of the semantics.

\begin{theorem}[Equivalence between additivity and distributivity]\label{th:equiv} $\;$
Let $C_1$, $C_2$ and $C'$ be programs. Assume for all $i \in [1, 3]$, there exists
a corresponding program $C_{P_i}$ such that 
  $\forall \; Q. \; \asem{C_{P_i}}(Q) = P_i$ holds. Then, 
\begin{multline*}
  \asem{(C_1 + C_2) \fcmp C_3}(P_1) = \asem{(C_1 \fcmp C_3) + (C_2 \fcmp C_3)}(P_1)
  \iff\\
  \asem{C'}(P_2 \join P_3) = \asem{C'}(P_2) \join \asem{C'}(P_3)\, .
\end{multline*}
  
\end{theorem}
\begin{proof} \ \
  \begin{itemize}
    \item[$(\impliedby)$]
      \begin{align*}
        \asem{(C_1 + C_2) \fcmp C_3}(P_1)
          &= \asem{C_3}(\asem{C_1}(P_1) \join \asem{C_2}(P_1)) \\
          &= \asem{C_3}(\asem{C_1}(P_1)) \join \asem{C_3}(\asem{C_2}(P_1)) \\
          &= \asem{(C_1 \fcmp C_3) + (C_2 \fcmp C_3)}(P_1)
      \end{align*}
    \item[$(\implies)$]
      \begin{align*}
        \asem{C'}(P_1 \join P_2) 
          &= \asem{C'}(\asem{C_{P_2}}(Q) \join \asem{C_{P_3}}(Q)) \\
          &= \asem{(C_{P_2} + C_{P_3}) \fcmp C'}(Q) \\
          &= \asem{(C_{P_2} \fcmp C) + (C_{P_3} \fcmp C')}(Q) \\
          &= \asem{C}(\asem{C_{P_2}}(Q)) \join \asem{C}(\asem{C_{P_3}}(Q)) \\
          &= \asem{C}(P_2) \join \asem{C}(P_3)
      \end{align*}
  \end{itemize}
\end{proof}

Theorem~\ref{th:equiv}  provides the intuition explaining why the above rule $\join$ fails:
in general, the
abstract inductive semantics lacks additivity, stemming from the non-additivity of 
the base commands.

\begin{theorem}[Additivity of the abstract inductive semantics] $\;$\\
  \label{thm:additivity}
  If, for all base commands $b$, $\bsem{b}^A(P_1 \join P_2) = \bsem{b}^A(P_1) \join \bsem{b}^A(P_2)$ then, for
  all programs $C$, 
  $\asem{C}(P_1 \join P_2) = \asem{C}(P_1) \join \asem{C}(P_2)$.
\end{theorem}
\begin{proof}
  By structural induction on $C$:
  \begin{itemize}
    \item $\sskip$:
      \begin{align*}
        \asem{\sskip}(P_1 \join P2)
          &= P_1 \join P_2 
          &\text{[By definition of $\asem{\cdot}$]} \\
          &= \asem{\sskip}(P_1) \join \asem{\sskip}(P_2)
          &\text{[By definition of $\asem{\cdot}$]} \\
      \end{align*}
    \item $b$:
      \begin{align*}
        \asem{b}(P_1 \join P2)
          &= \bsem{b}^A(P_1 \join P_2)
          &\text{[By definition of $\asem{\cdot}$]} \\
          &= \bsem{b}^A(P_1) \join \bsem{b}^A(P_2) \\
          &= \asem{b}(P_1) \join \asem{b}(P_2)
          &\text{[By definition of $\asem{\cdot}$]} \\
      \end{align*}
    \item $C_1 \fcmp C_2$:
      \begin{align*}
        \asem{C_1 \fcmp C_2}(P_1 \join P2)
          &= \asem{C_2}(\asem{C_1}(P_1 \join P_2)) \\
          &\text{[By definition of $\asem{\cdot}$]} \\
          &= \asem{C_2}(\asem{C_1}(P_1) \join \asem{C_1}(P_2)) \\
          &\text{[By inductive hypothesis]} \\
          &= \asem{C_2}(\asem{C_1}(P_1)) \join \asem{C_2}(\asem{C_1}(P_2)) \\
          &\text{[By inductive hypothesis]} \\
          &= \asem{C_1 \fcmp C_2}(P_1) \join \asem{C_1 \fcmp C_2}(P_2) \\
          &\text{[By definition of $\asem{\cdot}$]} \\
      \end{align*}
    \item $C_1 + C_2$:
      \begin{align*}
        \asem{C_1 \fcmp C_2}(P_1 \join P2)
          &= \asem{C_1}(P_1 \join P_2) \join \asem{C_2}(P_1 \join P_2) \\
          &\text{[By definition of $\asem{\cdot}$]} \\
          &= \asem{C_1}(P_1) \join \asem{C_1}(P_2) \join \asem{C_2}(P_1)
            \join \asem{C_2}(P_2) \\
          &\text{[By inductive hypothesis]} \\
          &= \asem{C_1}(P_1) \join \asem{C_2}(P_1) \join \asem{C_1}(P_2)
            \join \asem{C_2}(P_2) \\
          &= \asem{[C_1 + C_2]}(P_1) \join \asem{C_1 + C_2}(P_2) \\
          &\text{[By definition of $\asem{\cdot}$]} \\
      \end{align*}
    \item $C^\fix$:
      \begin{align*}
        \asem{C^\fix}(P_1 \join P2)
          &= \lfp(\lambda P' \to P_1 \join P_2 \join \asem{C}(P'))
          &\text{[By definition of $\asem{\cdot}$]}
      \end{align*}
      Let $F_i \defeq \bsem{C^\fix}(P_i) = \lfp(\lambda P' \to P_i \join 
      \asem{C}(P'))$

      We will show that $F_1 \join F_2$ is the $\lfp$ of the first equation.
      \begin{align*}
        (\lambda P' \to P_1 \join P_2 \join \asem{C}(P'))(F_1 \join F_2)
          &= P_1 \join P_2 \join \asem{C}(F_1 \join F_2) \\
          &= P_1 \join P_2 \join \asem{C}(F_1) \join \asem{C}(F_2)  \\
          &\text{[By inductive hypothesis]}\\
          &= P_1 \join \asem{C}(F_1) \join P_2 \join \asem{C}(F_2) \\
          &= F_1 \join F_2 \\
          &\text{[By definition of $F_i$]}\\
          &= \asem{C^\fix}(P_1) \join \asem{C^\fix}(P_2) \\
          &\text{[By definition of $F_i$]}\\
      \end{align*}

      Now we show that this fixpoint is indeed the least fixpoint. Let $P$ be any fixpoint, i.e.,
      $P = P_1 \join P_2 \join \asem{C}(P)$.
      Then, by definition of $\join$, we have that $P_i \join \asem{C}(P) \leq 
      P_1 \join P_2 \join \asem{C}(P)$. Since $F_i$ is the least fixpoint, we have that
      $F_i \leq P_i \join \asem{C}(P)$, thus, in turn,  $F_1 \join F_2 \leq P_1
      \join \asem{C}(P) \join P_2 \join \asem{C}(P) = P_1 \join P_2 \join 
      \asem{C}(P) = P$. Hence, $F_1 \join F_2$ is the least fixpoint.
  \end{itemize}
\end{proof}

We can provide a sufficient condition for the additivity of the abstract 
inductive semantics defined through a Galois insertion:
\begin{theorem}
  \label{thm:gamma-add}
  Let $\langle C, \sqsubseteq \rangle \galoiS{\alpha}{\gamma} \langle A, \leq 
  \rangle$ be a Galois insertion. If $\asem[C]{\cdot}$ and $\gamma$ are 
  additive functions then the abstract inductive semantics $\asem[A]{\cdot}$ induced 
  by the Galois insertion is additive as well.
\end{theorem}
\begin{proof}
  \begin{align*}
    \bsem{b}^A(P_1 \join P_2)
      &= \alpha(\bsem{b}^C(\gamma(P_1 \join P_2))) \\
      &= \alpha(\bsem{b}^C(\gamma(P_1))) \join\alpha(\bsem{b}^C(\gamma(P_1)))\quad \text{By additivity of $\gamma$, $\asem[C]{\cdot}$ and $\alpha$}\\   
      &= \bsem{b}^A(P_1) \join \bsem{b}^A(P_2)
  \end{align*}

  Then, by Theorem \ref{thm:additivity}, we conclude that $\asem{\cdot}$ is additive.
\end{proof}

We can also prove that the additivity of the abstract inductive
semantics is sufficient to ensure the soundness of the  rule $(\join)$.

\begin{theorem}[Soundness of the  rule $(\join)$]
  \label{thm:sound-join}
  If$\asem{\cdot}$ be additive then:
  $$\asem{C}(P_1) \leq Q_1 \text{ and } \asem{C}(P_2) \leq Q_2 \implies
  \asem{C}(P_1 \join P_2) \leq Q_1 \join Q_2\, .$$
\end{theorem}
\begin{proof}
  \begin{align*}
    \asem{C}(P_1 \join P_2)
      &= \asem{C}(P_1) \join \asem{C}(P_2)
      &\text{[By additivity of $\asem{\cdot}$]} \\
      &\leq Q_1 \join Q_2 
  \end{align*}
\end{proof}

Theorems \ref{thm:sound-join} and \ref{thm:gamma-add} correspond to the result
for Algebraic Hoare logic \cite[Theorem 6]{Cousot12}
showing that the rule $(\overline{\join})$ is sound under the
condition that $\gamma$ is additive.
A similar argument can be applied to ensure the soundness of the rule $(\meet)$ rule 
when the semantics is assumed to be co-additive.

Abstract domains that are both additive and co-additive are extremely rare,
especially for additivity alone, although they do exist. For instance, the
sign abstraction  depicted in Example \ref{exmp:sign} is one such domain,
guaranteeing the soundness of both merge rules.

\chapter{Backward Abstract Hoare Logic}

When defining the semantics for $\lang$, we implicitly assumed that the
abstract inductive semantics is defined in a forward fashion, as we defined $\asem{C_1
\fcmp C_2} \defeq \asem{C_2} \circ \asem{C_1}$. However, except for the rule
($\fcmp$), we never explicitly used this assumption. Thus, we can apply the theory of
Abstract Hoare logic to define a slight variation thereof, called Backward Abstract
Hoare logic, describing Hoare logics where the semantics is defined in a 
backward fashion. 

\section{Framework}

\subsection{Backward abstract inductive semantics}

To define the backward version of Abstract Hoare logic, we first need a
backward version of the underlying abstract inductive semantics.

\begin{definition}[Backward abstract inductive semantics]
  Given a complete lattice $A$ and a family of monotone functions $\bsem{\cdot}^A :
  \mathit{BCmd} \to A \to A$, the abstract inductive semantics $\asemback{\cdot}: \lang \to A \to A$
 is defined as
  follows:
%
  \begin{align*}
            \asemback{\sskip}        &\defeq id \\
      \asemback{b}             &\defeq \bsem{b}^A \\
      \asemback{C_1 \fcmp C_2} &\defeq \asemback{C_1} \circ \asemback{C_2} \\
      \asemback{C_1 + C_2}     &\defeq \lambda P . \asemback{C_1} P \join_A \asemback{C_2} P \\
      \asemback{C^\fix}        &\defeq \lambda P . \lfp(\lambda P'. P \join_A \asemback{C} P')
  \end{align*}
\end{definition}

Let us remark that the only difference with the abstract inductive semantics given in
Definition \ref{def:abstract-inductive-semantics} concerns the sequential composition $C_1 \fcmp
C_2$.
We can prove that the backward abstract inductive semantics is still monotone.

\begin{theorem}[Monotonicity]
  \label{thm:asem-mono-back} 
  For all $C \in \lang$, $\asemback{C}$ is well-defined and monotone.
\end{theorem}

\begin{proof}
  We modify the inductive case of the proof of Theorem \ref{thm:asem-mono} by
  providing only the case for $\asemback{C_1 \fcmp C_2}$, as all the other cases
  are identical.

  \begin{itemize}
    \item $C_1 \fcmp C_2$:

      By inductive hypothesis, $\asemback{C_2}$ is monotone, hence
      $\asemback{C_2}(P) \leq_A \asemback{C_2}(Q)$.

      \begin{align*}
        \asemback{C_1 \fcmp C_2}(P) 
          &= \asemback{C_1}(\asemback{C_2}(P))
          &\text{[By definition of $\asemback{C_1 \fcmp C_2}$]}\\
          &\leq_A \asemback{C_1}(\asemback{C_2}(Q))
          &\text{[By inductive hypothesis on $\asemback{C_1}$]} 
      \end{align*}
  \end{itemize}
\end{proof}

\subsection{Backward Abstract Hoare Logic}

We can give a corresponding definition of backward abstract Hoare triple,
which is the same as for abstract Hoare triples except for the fact that the backward
abstract inductive semantics is used. 

\begin{definition}[Backward Abstract Hoare triple]
  \label{def:baht}
  Given an abstract inductive semantics $\asemback{\cdot}$ on the complete
  lattice $A$, the backward abstract Hoare triple denoted by 
  $\atripleback{P}{C}{Q}$ is
  valid when $\asemback{C}(P) \leq_A Q$ holds, namely, 
%
  $$\models \atripleback{P}{C}{Q} \iff \asemback{C}(P) \leq_A Q\, .$$
\end{definition}

Intuitively now the roles of $P$ and $Q$ are reversed, in Hoare logic and
Abstract Hoare logic $P$ was a precondition and $Q$ was a postcondition, in
Backward Abstract Hoare logic instead $P$ is a postcondition and $Q$ a 
precondition.

Clearly, the proof system only needs to be modified to accommodate the new
semantics for program composition, while the other rules are unchanged.

\begin{definition}[Backward Abstract Hoare rules]$\;$\\
  We provide the rule for sequential composition only---all the other rules are
  given in Definition \ref{def:ahtrules}.

  % Rule for sequential composition
  \begin{prooftree}
    \AxiomC{$\vdash \atripleback{P}{C_2}{Q}$}
    \AxiomC{$\vdash \atripleback{Q}{C_1}{R}$}
    \RightLabel{$(\mathbb{\fcmp})$}
    \BinaryInfC{$\vdash \atripleback{P}{C_1 \fcmp C_2}{R}$}
  \end{prooftree}
\end{definition}

The above composition rule can be intuitively read as follows: 
If executing backward $C_2$ from state $P$ leads to a state $Q$,
and executing backward $C_1$ from state $Q$ leads to a state $R$, then executing backward $C_2$
followed by $C_1$ from state $P$ leads to the state $R$. 
We can prove soundness and completeness of this backward proof system.

\begin{theorem}[Soundness]
  \label{thm:atriple-sound-back}
  $$\vdash \atripleback{P}{C}{Q} \;\implies\; \models \atripleback{P}{C}{Q}$$
\end{theorem}

\begin{proof}
  We modify the inductive case of the proof of Theorem \ref{thm:atriple-sound}
  by providing only the case for rule $(\fcmp)$ as all the other cases are
  identical.
The last step in the derivation is as follows:
        \begin{prooftree}
          \AxiomC{$\vdash \atripleback{P}{C_2}{Q}$}
          \AxiomC{$\vdash \atripleback{Q}{C_1}{R}$}
          \RightLabel{$(\mathbb{\fcmp})$}
          \BinaryInfC{$\vdash \atripleback{P}{C_1 \fcmp C_2}{R}$}
        \end{prooftree}
          
        \noindent  
        By inductive hypothesis:
        $\asemback{C_2}(P) \leq_A Q$ and
        $\asemback{C_1}(Q) \leq_A R$.
        The triple is valid because:
        \begin{align*}
          \asemback{C_1 \fcmp C_2}(P)
            &= \asemback{C_1}(\asemback{C_2}(P))
            &\text{[By definition of $\asemback{\cdot}$]} \\
            &\leq_A \asemback{C_1}(Q)
            &\text{[By monotonicity of $\asemback{\cdot}$]} \\
            &\leq_A R
        \end{align*}
\end{proof}

\begin{theorem}[Relative $\asemback{\cdot}$-completeness]
  \label{thm:post-completeness-back}
  $$\vdash \atripleback{P}{C}{\asemback{C}(P)}$$
\end{theorem}

\begin{proof}
  We modify the inductive case of the proof of Theorem
  \ref{thm:post-completeness} by providing only the case for $C_1 \fcmp C_2$, as
  all the other cases are identical.

\noindent
        By definition $\asemback{C_1 \fcmp C_2}(P) = \asemback{C_1}(\asemback{C_2}(P))$

        \begin{prooftree}
          \AxiomC{(Inductive hypothesis)}
          \noLine
          \UnaryInfC{$\vdash \atripleback{P}{C_2}{\asemback{C_2}(P)}$}
          \AxiomC{(Inductive hypothesis)}
          \noLine
          \UnaryInfC{$\vdash \atripleback{\asemback{C_2}(P)}{C_1}{\asemback{C_1}(\asemback{C_2}(P))}$}
          \RightLabel{($\fcmp$)}
          \BinaryInfC{$\vdash \atripleback{P}{C_1 \fcmp C_2}{\asemback{C_1 \fcmp C_2}(P)}$}
        \end{prooftree}
\end{proof}

\begin{theorem}[Relative completeness]
  $$\models \atripleback{P}{C}{C} \implies\; \vdash \atripleback{P}{C}{Q}$$
\end{theorem}
\begin{proof}
  By definition of $\models \atripleback{P}{C}{Q} \iff Q \geq_A \asemback{C}(P)$, we have that:
%
  \begin{prooftree}
    \AxiomC{$P \leq_A P$}
    \AxiomC{(By Theorem \ref{thm:post-completeness-back})}
    \noLine
    \UnaryInfC{$\vdash \atripleback{P}{C}{\asemback{C}(P)}$}
    \AxiomC{$Q \geq_A \asemback{C}(P)$}
    \RightLabel{$(\leq)$}
    \TrinaryInfC{$\vdash \atripleback{P}{C}{Q}$}
  \end{prooftree}
\end{proof}

\section{Instantiations}

\subsection{Partial Incorrectness, Again}

An abstract inductive semantics induces systematically a backward abstract
inductive semantics where the semantics of the basic commands is inverted.

\begin{definition}[Reverse Abstract Inductive Semantics]
  Given an abstract inductive semantics defined on some complete lattice $A$
  with basic command semantics $\bsem{\cdot}^A$, we can define the reverse
  backward abstract inductive semantics as the backward inductive semantics
  instantiated on the complete lattice $A$ and with the semantics of 
  basic commands defined by: 
  $(\bsem{\cdot}^A)^{-1}$.
\end{definition}

Accordingly, the reverse abstract inductive semantics is defined as follows:
\begin{align*}
  \asemback{\sskip}        &= id \\
  \asemback{b}             &= (\bsem{b}^A)^{-1} \\
  \asemback{C_1 \fcmp C_2} &= \asemback{C_1} \circ \asemback{C_2} \\
  \asemback{C_1 + C_2}     &= \lambda P . \asemback{C_1} P \join_A \asemback{C_2} P \\
  \asemback{C^\fix}        &= \lambda P . \lfp(\lambda P'. P \join_A \asemback{C} P')
\end{align*}

According to the intuition that the abstract inductive semantics is an abstract
version of the strongest postcondition, which intuitive interpretation should we give to
reverse abstract inductive semantics? This construction corresponds to the
abstract version of the weakest precondition. In fact, when the dual reverse
inductive semantics is obtained from the abstract inductive semantics on
$\pow{\states}$ (i.e., the strongest postcondition), the reverse semantics becomes
the weakest precondition.
Hence, from the validity of the corresponding triples, we have that: 
$$\models
\atripleback[\pow{\states}]{P}{C}{Q} \iff \asemback[\pow{\states}]{C}(P)
\subseteq Q \iff wp(C, P) \subseteq Q\, .$$

This program logic has been studied in \cite{Ascari24} under the name of NC, and
it is indeed equivalent to the logic described in Section
\ref{chp:partial-incorrectness}.

\subsection{Hoare Logic, Again}

Following Section \ref{chp:partial-incorrectness}, we can first
obtain the reverse semantics, and next the dual of the reverse
semantics. This latter semantics is therefore defined as follows: 
\begin{align*}
  \asemback[A^{\mathrm{op}}]{\sskip}        &= id \\
  \asemback[A^{\mathrm{op}}]{b}             &= (\bsem{b}^A)^{-1} \\
  \asemback[A^{\mathrm{op}}]{C_1 \fcmp C_2} &= \asemback{C_1} \circ \asemback{C_2} \\
  \asemback[A^{\mathrm{op}}]{C_1 + C_2}     &= \lambda P . \asemback[A^{\mathrm{op}}]{C_1} P \meet_A \asemback[A^{\mathrm{op}}]{C_2} P \\
  \asemback[A^{\mathrm{op}}]{C^\fix}        &= \lambda P . \gfp_A(\lambda P'. P \meet_A \asemback[A^{\mathrm{op}}]{C} P')
\end{align*}

This definition corresponds to the reverse inductive semantics obtained from
the abstract inductive semantics, which is the abstract version of the weakest
liberal precondition. In fact, when the dual is applied to $\pow\states$ (the
strongest postcondition), the reverse semantics becomes the weakest liberal
precondition. This can be easily seen by looking at the definition for the
non-deterministic choice and the loop commands: if we interpret the input of
the semantics as the final state, we are computing all the states that must
reach (up to termination) the final states.

Hence, from the validity of the triples we obtain:
$$\models \atripleback[\pow{\states}^{\mathrm{op}}]{P}{C}{Q} \iff
\asemback[\pow{\states}]{C}(P) \supseteq Q \iff wlp(C, P) \supseteq Q$$

\noindent
We  also have that $wlp(C, P) \supseteq Q \iff \sem{C}(Q) \subseteq P$, hence this is
equivalent to Hoare logic.

\chapter{Conclusions}

In this thesis, we extended the ubiquitous 
traditional Hoare logic by transforming it into an abstract and
versatile framework to be instantiated to design novel program logics. 
By following well-known abstract interpretation principles, 
we developed a general methodology for reasoning about a broader range of program properties.
Our study demonstrated that multiple program logics known in
literature can be viewed as instantiations of Abstract Hoare Logic. Notably, 
while constructing a program logic for hyperproperties in our general framework,
we provided a novel compositional definition of the strongest hyper
postcondition.
Furthermore, we showed how the core proof principles of Hoare logic can be
applied to proving an underapproximation of program properties. In particular, this highlighted
some fundamental differences with the Incorrectness Logic proof system: 
the infinitary loop rule required for the relative completeness of Incorrectness Logic:
%
\begin{prooftree}
  \AxiomC{$[p(n)] \; C \; [p(n + 1)]$}
  \UnaryInfC{$[p(0)] \; C^\star \; [ \exists n . p(n)]$}
\end{prooftree}
%
is not due to the fact that Incorrectness Logic aims at proving 
an underapproximation but rather
because Incorrectness Logic is  a ``total correctness logic'', meaning that it inherently carries 
a proof of termination.
We also studied the requirements to introduce frame-like rules in Abstract
Hoare Logic and how to obtain a backward variant of this framework. 

\section{Future work}
As stimulating directions of future work, we plan the investigate the 
following questions. 
%are only preliminary results that we weren't able to explore
%because of time constraints.

\paragraph{\textbf{Total correctness/Incorrectness logics.}}
We have shown how all the partial correctness/incor\-rectness triples are
instances of (backward) Abstract Hoare Logic and use a very similar proof
system. To complete the picture presented in \cite{Zhang22}, we are missing the
total correctness and incorrectness logics, ??? and ?`?`?`. Since their
relationship is analogous to that between partial correctness and incorrectness
logics, the same abstraction used to transform Hoare Logic into Abstract Hoare
Logic could be used to transform Incorrectness Logic \cite{Moller21} into
Abstract Incorrectness Logic. By abstracting the proof system, we can obtain a
sound and relatively complete proof system for Abstract Incorrectness Logic.
Then, by reusing the same technique applied here to Abstract Hoare Logic to
invert the semantics and the lattice, we can obtain all the four program logics
that are missing, therefore completing the whole spectrum of possible logics.

\paragraph{\textbf{Hyper domains.}}
We investigated hyper domains to encode the strongest hyper postcondition,  and,
correspondingly, we obtained
a Hoare-like logic for hyperproperties. We have shown how we can use the
abstract inductive semantics to model the strongest liberal postcondition,
weakest precondition, and weakest liberal precondition. We could apply the
same technique to  the abstract inductive semantics instantiated with a hyper
domain of $\pow{\states}$, to study whether this would  lead to some interesting novel 
logics or if
they are all equivalent (this could happen because hyperproperties can disprove themselves,
meaning that if a triple in hyper Hoare logic is false we can prove its negation).

An interesting feature of the hyper Hoare logic obtained via Abstract Hoare Logic
is that the assertion language is relatively low-level, making it cumbersome to
use for proving actual hyperproperties. The proof system given in \cite{Darnier2023}
is actually quite similar to the one obtained with the hyper domains, but the
Exist rule is missing. If the goal is that of proving the completeness of Hyper
Hoare Logic, then the Exist rule must be embedded somewhere in the rules of Abstract Hoare
Logic.

\paragraph{\textbf{Unifying Forward and Backward Reasoning.}}
The only difference between Abstract Hoare Logic and Backward Abstract Hoare
Logic lies in the abstract inductive semantics, where the semantics of program
composition is inverted. A potential solution would be to make the
semantics parametric on the composition $\asem{C_1 \fcmp C_2} \defeq \asem{C_1}
\star \asem{C_2}$ and let $P \star Q= Q \circ P$ for the forward semantics and
$P \star Q = P \circ Q$ for the backward semantics. However, this approach would not be uniform
when defining the command composition rule for the proof system.

\section{Related work}

The idea of systematically constructing program logics, of course, is not new. Kleene
Algebra with Tests (KAT) \cite{Kozen97} was one of the first works of this
kind. In Section \ref{chp:join-meet-rules}, we discussed how, in general, we
cannot distribute the non-deterministic choice (i.e., $\asem{(C_1 + C_2) \fcmp C_3} \neq
\asem{(C_1 \fcmp C_3) + (C_2 \fcmp C_3)}$), thus violating one of the axioms of
Kleene algebras. A similar alternative was investigated in \cite{Martin06},
using traced monoidal categories to encode properties of the program. For
example, the monoidal structure is used to model non-deterministic choice but
imposes the same distributivity requirements as Kleene Algebras (this is caused
by $\oplus$ being a bifunctor). However, disregarding expressivity, the main
difference lies in the philosophy behind the approach. Abstract Hoare Logic is
a more semantics-centered approach instead of being an ``equational'' theory like
KAT. This semantics-centered approach was also pivotal in providing the idea that
abstract inductive semantics could be used not only to encode the strongest
postcondition but also the strongest liberal postcondition, weakest
precondition, and weakest liberal precondition, thereby unifying all these partial (in)-correctness 
Hoare-like logics. 

The fundamental approach of Outcome Logic
\cite{Zilberstein23} is similar to 
that of Abstract Hoare Logic. Like Abstract Hoare Logic, the semantics of the language
in Outcome Logic is parametric on the domain of execution, although the assertion
language is fixed if we ignore the basic assertions on program states. Outcome
Logic originally aimed to unify correctness and incorrectness reasoning with
the powerset instantiation, and has not be conceived to be a minimal theory for sound and complete
Hoare-like logics. In fact, Outcome Logic does not bring a result of (relative) completeness. As
discussed in \cite{Darnier2023}, Outcome Logic with the powerset instantiation
is actually a proof system for 2-hyperproperties (namely, hyperproperties regarding at
most two executions). Thus, Outcome triples can be proved in the instantiation
of Abstract Hoare Logic provided in section \ref{chp:hyper}, even though it
would be interesting to find a direct encoding of Outcome Logic in terms of
Abstract Hoare Logic.

% Following sections will not be imported and therefore not printed
% \import{./proofs}{mod}
% \import{./conclusions}{mod}

\backmatter
\cleardoublepage
\phantomsection
\pdfbookmark{Abstract}{Abstract}

\begingroup

\let\clearpage\relax
\let\cleardoublepage\relax

%% \chapter*{Bibliography}
%% \nocite{*} % if you want to print all the references

%% Print biblio
\printbibliography

\endgroup

\vfill
\end{document}