\documentclass[11pt,a4paper]{scrartcl}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage[utf8]{inputenc}
\usepackage[margin=2.25cm]{geometry}
\usepackage{hyperref}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{lmodern}
\usepackage{booktabs}
\usepackage{graphicx}
\usepackage{float}
\usepackage{tikz}
\usepackage{listings}
\usepackage{pgfplots}
\pgfplotsset{compat=1.18}
\usepackage{subcaption}
\setlength{\parindent}{0cm}
\setlength{\parskip}{0.3em}
\hypersetup{pdfborder={0 0 0}}
%\usepackage[nomessages]{fp} no easter eggs this time
\usepackage{amsmath}
\DeclareMathOperator*{\argmax}{arg\,max}
\DeclareMathOperator*{\argmin}{arg\,min}
\usepackage{minted}

\renewcommand{\MintedPygmentize}{python3 ./pygmentize.py}

\definecolor{codegreen}{rgb}{0,0.6,0}
\definecolor{codegray}{rgb}{0.5,0.5,0.5}
\definecolor{codepurple}{rgb}{0.58,0,0.82}
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}

\lstdefinestyle{mystyle}{
  backgroundcolor=\color{backcolour},   
  commentstyle=\color{codegreen},
  keywordstyle=\color{magenta},
  keywordstyle=[2]{\color{olive}},
  numberstyle=\tiny\color{codegray},
  stringstyle=\color{codepurple},
  basicstyle=\ttfamily\footnotesize,
  breakatwhitespace=false,         
  breaklines=true,                 
  captionpos=b,  
  keepspaces=true,                 
  numbers=left,  
  numbersep=5pt,
  showspaces=false,                
  showstringspaces=false,
  showtabs=false,
  tabsize=2,
  aboveskip=0.8em,
  belowcaptionskip=0.8em
}
\lstset{style=mystyle}

\geometry{left=2cm,right=2cm,top=2cm,bottom=3cm}
\title{
\vspace{-5ex} 
Assignment 1 -- Software Analysis \\\vspace{0.5cm}
\Large Deductive verification with Dafny
\vspace{-1ex} 
}
\author{Claudio Maggioni}
\date{\vspace{-3ex}}

\begin{document}
\maketitle
\tableofcontents

\section{Choice of Sorting Algorithm}

I decide to implement and verify the correctness of selection sort. The
algorithm sorts a given list in place with average and worst-case complexity
$O(n^2)$. It works by iteratively finding either the minimum or maximum element
in the list, pushing it to respectively either the beginning or the end of the
list, and subsequently running the next iteration over the remaining $n-1$
elements.

For the sake of this assignment, I choose to implement and analyze the variant
where the minimum element is computed. The pseudocode of selection sort is given
in algorithm \ref{alg:sel}.

\begin{algorithm}
  \caption{Selection sort}\label{alg:sel}
  \begin{algorithmic}[1]
  \Require $a$ list of values 
  \Ensure $a$ is sorted in-place
  \If{$a = \emptyset$}
    \State \Return
  \EndIf
  
  \State $s \gets 0$
  \While{$s < |a|$}
    \State {$m \gets \argmin_x{a[x]}$ for $s \leq x < |a|$}
    \State {\textbf{swap} $a[x]$, $a[s]$}
    \State {$s \gets s + 1$}
  \EndWhile
  \end{algorithmic}
\end{algorithm}

I choose this algorithm due to its procedural nature, since I feel more
comfortable tackling loops instead of recursive calls when writing verification
code as we already covered them in class.

Additionally, given the algorithm incrementally places a ever-growing portion of
sorted elements at the beginning of the list as $s$ increases, finding a loop
invariant for the \textbf{while} loop shown in the pseudocode should be simple
as I can formalize this fact into a predicate.

\subsection{Dafny implementation}

To implement and verify the algorithm I use
\href{https://dafny.org/}{\color{blue} Dafny}, a programming language that is
verification-aware and equipped with a static program verifier.

I first write an implementation of the pseudocode, listed below.

\begin{listing}[H]
\begin{minted}[linenos]{dafny}
method SelectionSort(a: array<int>) 
{
  if (a.Length == 0) {
    return;
  }
  
  var s := 0;

  while (s < a.Length - 1) 
  {
    var min: int := s;
    var i: int := s + 1;

    while (i < a.Length)
    {
      if (a[i] < a[min]) {
        min := i;
      }
      i := i + 1;
    }

    a[s], a[min] := a[min], a[s];
    s := s + 1;
  }
}
\end{minted}
    \caption{Implementation of selection sort in Dafny}
    \label{lst:sel}
\end{listing}

The implementation is only slightly different from the pseudocode. The biggest
difference lies in the inner \textbf{while} loop at lines 14-20. This is just a
procedural implementation of the assignment

$$m \gets \argmin_x{l[x]} \text{\hspace{1cm} for \hspace{1cm}} s \leq x < |l|$$

at line 6 of the pseudocode.

\section{Verification}

I now verify that the implementation in listing \ref{lst:sel} is correct by
adding a specification to it, namely a method precondition, a method
postcondition, and invariants and variants for the outer and inner loop.

\subsection{Method precondition and postcondition}

Aside the \mintinline{dafny}{array<int>} type declaration, no other condition is
needed to constrain the input parameter \texttt{a} as a sorting algorithm should
sort any list. Therefore, the method precondition is

\begin{center}
\mintinline{dafny}{requires true}
\end{center}

which can just be omitted.

Regarding postconditions, as the assignment description suggests, we need to
verify that the method indeed sorts the values, while preserving the values in
the list (i.e. without adding or deleting values).

We can define the sorted condition by saying that for any pair of monotonically
increasing indices of $a$ the corresponding elements should be monotonically
non-decreasing. This can be expressed with the predicate:

\begin{minted}{dafny}
predicate sorted(s: seq<int>)
{
  forall i,j: int :: 0 <= i < j < |s| ==> s[i] <= s[j]
}
\end{minted}

According to advice given during lecture, we can express order-indifferent
equality with the predicate:

\begin{minted}{dafny}
predicate sameElements(a: seq<int>, b: seq<int>)
{
  multiset(a) == multiset(b)
}
\end{minted}

Therefore, the method signature including preconditions and postconditions
is:

\begin{minted}{dafny}
method SelectionSort(a: array<int>) 
  modifies a
  ensures sorted(a[..])
  ensures sameElements(a[..], old(a[..]))
\end{minted}

\subsection{Outer loop variant and invariant}
{\color{red}TBD}

\subsection{Inner loop variant and invariant}
{\color{red}TBD}


\begin{verbatim}
Did you introduce some that you then realized were not needed?

Any details of the algorithm’s implementation that you may have had to adjust to
make specification or verification easier.
 > if list is empty

What were the hardest steps of the verification process?
\end{verbatim}

\end{document}