\documentclass{llncs}

\usepackage{graphicx}
\usepackage{array}
\usepackage{cellspace}
\usepackage{xspace}
\usepackage{color, colortbl}
\usepackage{url}
\usepackage{./gospel}
% \usepackage{fullpage}

\usepackage{hyperref}

\input{./mymacros.tex}

\newcommand{\cameleer}{\textsf{Cameleer}\xspace}

\renewcommand{\check}{
  \raisebox{-.25\height}{\includegraphics[width=1em,height=1em]{check.png}}}

\newcommand{\cross}{
  \raisebox{-.25\height}{\includegraphics[width=1em,height=1em]{cross.png}}}

% \newcommand{\ocaml}{\textsf{OCaml}\xspace}
% \newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\GOSPEL}{{\textsf{GOSPEL}}\xspace}

\newcommand{\todo}[1]{\textbf{TODO:}#1}

\definecolor{thegray}{rgb}{0.849,0.849,0.849}

\title{\cameleer\xspace -- Case Studies}
\author{M\'ario Pereira}
\institute{NOVA LINCS \& Nova School of Science and Technology,
  Portugal}
\date{Working version of \today}

\begin{document}

\maketitle

\begin{abstract}
  This is a working document where I maintain a list of all \ocaml examples that
  are fully verified by the \cameleer
  tool\footnote{\url{https://github.com/mariojppereira/cameleer}}. For each case
  study, I provide relevant numerical and proof effort metrics. All of
  the listed examples are available at the project's \textsf{GitHub\xspace}
  repository, under the \texttt{examples} directory. Working version of \today.
\end{abstract}

\begin{figure}
  \centering
  \begin{tabular}
    {>{\raggedright}m{.33\textwidth}|>
    {\centering}m{.1\textwidth}|>
    {\centering}m{.275\textwidth}|c|Sc}
    Case study               & \# VCs & LOC / Spec. / Ghost & Proof time
    & Immediate \\\hline
    Applicative Queue        & 23     & 25  / 17 / 4        & 1.90  & \check \\
    \rowcolor{thegray}
    Arithmetic Compiler      & 258    & 235 / 48 / 155      & 18.96 & \cross \\
    Binary Multiplication    & 12     & 10  / 6  / 0        & 0.79  & \check \\
    \rowcolor{thegray}
    Binary Search            & 37     & 62 / 40 / 0         & 1.54  & \check \\
    Binary Search Trees      & 33     & 20 / 26 / 0         & 1.34  & \cross \\
    \rowcolor{thegray}
    Checking a Large Routine & 16     & 25 / 15 / 0         & 0.80  & \check \\
    CNF Convertion           & 124    & 113 / 47 / 0        & 5.34  & \check \\
    \rowcolor{thegray}
    \rowcolor{thegray}
    Duplicates in an Array   & 11     & 10  / 9  / 0        & 0.59  & \check \\
    Ephemeral Queue          & 44     & 40  / 29 / 7        & 1.87  & \check \\
    \rowcolor{thegray}
    Even-odd Test            & 6      & 6 / 8 / 0           & 0.60  & \check \\
    Factorial                & 8      & 10 / 9 / 0          & 0.58  & \check \\
    \rowcolor{thegray}
    Fast Exponentiation      & 5      & 4 / 4 / 0           & 0.57  & \check \\
    Fibonacci                & 15     & 16 / 15 / 2         & 0.79  & \check \\
    \rowcolor{thegray}
    FIND Algorithm           & 6      & 13 / 7 / 0          & 0.61  & \check \\
    Insertion Sort           & 30     & 13 / 34 / 0         & 2.56  & \check \\
    \rowcolor{thegray}
    Integer Square Root      & 11     & 8 / 14 / 0          & 0.80  & \check \\
    Leftist Heap             & 133    & 99 / 179 / 0        & 5.70  & \check \\
    \rowcolor{thegray}
    Mjrty                    & 25     & 33 / 12 / 0         & 1.31  & \check \\
    \ocaml List.fold\_left   & 26     & 5  / 20 / 0         & 1.75  & \cross \\
    \rowcolor{thegray}
    \ocaml Stack             & 22     & 25 / 27 / 1         & 1.01  & \check \\
    Pairing Heap             & 68     & 65 / 101 / 25       & 3.60  & \cross \\
    \rowcolor{thegray}
    Program Proofs           & 63     & 93 / 54 / 24        & 1.94  & \cross \\
    Same Fringe              & 23     & 22 / 16 / 0         & 0.82  & \check \\
    \rowcolor{thegray}
    Small-step Iterators     & 51     & 43 / 50 / 2         & 6.53  & \cross \\
    Tree Height CPS          & 4      & 8  / 8  / 0         & 0.67  & \check \\
    \rowcolor{thegray}
    Union Find               & 63     & 36 / 29 / 7         & 3.93  & \check
  \end{tabular}
  \caption{Summary of the case studies verified with the \cameleer tool.}
  \label{figure:case-studies}
\end{figure}

\section{Case Studies}
\label{sec:case-studies}

The complete set of case studies verified with the \cameleer tool is depicted in
Fig.~\ref{figure:case-studies}. All of these are fully verified, using a
combination of the Alt-Ergo, CVC4, and Z3 SMT solvers. For each example I
provide, in order, the following metrics:
%
\begin{enumerate}
\item The number of verification conditions generated by \why, for that proof.
\item The number of \ocaml lines of code, \GOSPEL lines of code, and ghost lines
  of code. Ghost code includes ghost record fields, ghost functions, and lemma
  functions. It is worth noting that ghost code is regular \ocaml code, hence
  ghost LOC are already included in the \ocaml LOC measure.
\item The proof time it takes (measured in seconds), in order to successfully
  replay the proof.
\item A visual indication that tells whether or not manual interaction is
  required in order to complete the proof. The (\check) sign marks a proof
  that requires no extra user interaction, other than writing down the \GOSPEL
  specification.
\end{enumerate}
%
In the following, I briefly describe each case study.

\subsection{Applicative Queue}
\label{sec:applicative-queue}

A FIFO data structure implemented \textit{à la Baker}, \emph{i.e.}, it stores
the elements in the Queue using two different lists. The first such list stores
the elements in order, while the second one stores them in reverse order. This
is captured by the following type definition:
%
\begin{gospel}
  type 'a t = {
    self : 'a list * 'a list;
    view : 'a list [@ghost];
  }
\end{gospel}
%
The \of{view} ghost field is used as a logical model of the data structure. This
is connected to the real field \of{self} via the following type invariant:
%
\begin{gospel}
    (*@ invariant let prefix, xiffus = self in
                  (prefix = [] -> xiffus = []) &&
                  view = prefix @ List.rev xiffus *)
\end{gospel}
%
The first part of the invariant provides a very simple criteria to test the
queue for emptiness, as follows:
%
\begin{gospel}
  let [@logic] is_empty {self; _} = match self with
    | [], _ -> true
    | _ -> false
  (*@ b = is_empty q
        ensures b <-> q.view = [] *)
\end{gospel}
%
New elements are always pushed to the head of the second list of the \of{self}
field \emph{except} when the queue is empty, so to respect the type
invariant. This is as follows:
%
\begin{gospel}
  let add elt {self; view} = match self with
    | [], [] ->
        { self = [elt], []; view = [elt] }
    | prefix, xiffus ->
        { self = prefix, elt :: xiffus; view = view @ [elt] }
  (*@ r = add elt queue
        ensures r.view = queue.view @ (elt :: []) *)
\end{gospel}
%
Note the update of the \of{view} field, which boils down here to append the new
element \of{elt} to the end of the list. This is inefficient but it does not
jeopardize the expected complexity of this FIFO structure: this is ghost code
hence it should be erased before compilation.

Elements are popped from the queue as follows:
%
\begin{gospel}
  let tail {self; view} = match self with
    | [_], xiffus ->
        { self = List.rev xiffus, []; view = tail_list view }
    | _ :: prefix, xiffus ->
        { self = prefix, xiffus; view = tail_list view }
    | [], _ -> raise Not_found
  (*@ r = tail t
        raises  Not_found -> is_empty t
        ensures r.view = tail_list t.view *)
\end{gospel}
%
The \of{tail} function runs in $O(1)$ when there is more than one stored
element; it runs in $O(n)$ when the queue has more than one element, where $n$
is the size of the second list in \of{self}. It is this behavior of \of{tail}
that provides an amortized execution complexity to a sequence of
\of{head}-\of{tail} operations.

Function \of{tail} raises the \of{Not_found} exception (from the \ocaml standard
library) whenever the queue is empty. In order to update the \of{view} model, we
use the \of{tail_list} function. This removes the last element of the \of{view}
list, as follows:
%
\begin{gospel}
  let [@ghost] [@logic] tail_list = function
    | [] -> assert false
    | _ :: l -> l
  (*@ r = tail_list q
        requires q <> []
        ensures  match q with [] -> false | _ :: l -> r = l *)
\end{gospel}
%
The above definition works only for non-empty queues, hence the given
precondition. As such, the \of{assert false} expression marks a provable
unreachable point in the code. Since function \of{tail_list} is only used to
manipulate field \of{view}, we declare it as a ghost function. Also, and in
order to provide a more concise and readable postcondition to function
\of{tail}, we attach the \of{[@logic]} attribute to \of{tail_list}. This make it
a functional symbol available both in specification and program.

This \ocaml module features two more functions with the following type and
contract:
%
\begin{gospel}
  val empty : 'a t
  (*@ t = empty
        ensures t.view = [] *)

  val head : 'a t -> 'a
  (*@ x = head param
        raises  Not_found -> is_empty param
        ensures match param.view with [] -> false | y :: _ -> x = y *)
\end{gospel}
%
It is worth noting that this case study is issued from the OCamlGraph library
source code
\footnote{\scriptsize\url{https://github.com/backtracking/ocamlgraph/blob/master/src/lib/persistentQueue.ml}}.
Interestingly, the type invariant is provide as an informal comment in the
library code.

\subsection{Arithmetic Compiler}
\label{sec:arithmetic-compiler}

A simple compiler from arithmetic expressions into a stack machine. This case
study is loosely inspired by the Nielsons' textbook ``Semantics with
Applications: an Appetizer''.

\todo

\subsection{Binary Multiplication}
\label{sec:binary-mult}

\todo

\subsection{Binary Search}
\label{sec:binary-search}

\todo

\subsection{Binary Search Tree}
\label{sec:binary-search-tree}



\subsection{Checking a Large Routine}
\label{sec:check-large-rout}

\todo

\subsection{CNF Conversion}
\label{sec:cnf-conversion}

\todo

\subsection{Duplicates in an Array}
\label{sec:duplicates-an-array}

\todo

\subsection{Ephemeral Queue}
\label{sec:ephemeral-queue}

\todo

\subsection{Even-odd Test}
\label{sec:even-odd-test}

\todo

\subsection{Factorial}
\label{sec:factorial}

\todo

\subsection{Fast Exponentiation}
\label{sec:fast-exponentiation}

\todo

\subsection{Fibonacci}
\label{sec:fibonacci}

\todo

\subsection{FIND Routine}
\label{sec:find-routine}

\todo

\subsection{Insertion Sort}
\label{sec:insertion-sort}

\todo

\subsection{Integer Square Root}
\label{sec:integer-square-root}

\todo

\subsection{Leftist Heap}
\label{sec:leftist-heap}

\todo

\subsection{Mjrty Algorithm}
\label{sec:mjrty-algorithm}

\todo

\subsection{\ocaml List.fold\_left}
\label{sec:ocaml-list.fold_left}

\todo

\subsection{\ocaml Stack}
\label{sec:ocaml-stack}

\todo

\subsection{Pairing Heap}
\label{sec:pairing-heap}

\todo

\subsection{Program Proofs}
\label{sec:program-proofs}

\todo

\subsection{Same Fringe}
\label{sec:same-fringe}

\todo

\subsection{Small-step Iterators}
\label{sec:small-step-iterators}

\todo

\subsection{Tree Height in CPS}
\label{sec:tree-height-cps}

\todo

\subsection{Union Find}
\label{sec:union-find}

\todo

\end{document}
