343 lines
12 KiB
TeX
343 lines
12 KiB
TeX
\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
|
|
|
|
\section{Choice of Sorting Algorithm}
|
|
|
|
In order to choose I browse the implementations of some classical sorting
|
|
algorithms to find one that strikes a good tradeoff between ease-of-proof and a
|
|
solid understanding of how it works on my part.
|
|
|
|
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
|
|
\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 3 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
|
|
|
|
\mintinline{dafny}{requires true}
|
|
|
|
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}
|
|
|
|
As mentioned already, the outer \textbf{while} loop in selection sort strongly
|
|
relates with the incremental selection of minimum values from the non-processed
|
|
part of the list (i.e. for indices in $[s,|a|)$) and them being moved to the
|
|
beginning of the list in the correct order. Indeed, the outer loop maintains two
|
|
main properties:
|
|
|
|
\begin{itemize}
|
|
\item The processed elements (i.e. indices $[0, s)$) are sorted, as the elements
|
|
in them are the minimum, the second-minimum, the third-minimum and so on in
|
|
this order;
|
|
\item As all the processed elements have been selected as minimums, all of them
|
|
are by definition greater than or equal than the non-processed elements.
|
|
Even if this property seems trivial, it is quite important to ensure we
|
|
can simply ``append'' elements to the processed portion as they will for
|
|
sure be greater than all the values in indices $[0, s)$.
|
|
\end{itemize}
|
|
|
|
We can formalize these two facts respectively with two Dafny loop invariants on
|
|
the outer while loop:
|
|
|
|
\begin{minted}{dafny}
|
|
invariant s >= 1 ==> sorted(a[0..s]) // saying one item is sorted makes little sense
|
|
invariant forall i,j: int :: 0 <= i < s <= j < a.Length ==> a[i] <= a[j]
|
|
\end{minted}
|
|
|
|
Since this loop has an index $s$ iterating over the values in $[0,|a| - 1]$
|
|
(note that we condiser the value of $s$ after loop termination as well) in
|
|
steps of one the corresponding loop invariant and variant on the index are quite
|
|
straightforward\footnote{We specify loop variants as well for completeness'
|
|
sake, even if Dafny is able to infer them in these circumnstances.}. Indeed,
|
|
they are respectively:
|
|
|
|
\begin{minted}{dafny}
|
|
invariant s <= a.Length - 1
|
|
decreases a.Length - s
|
|
\end{minted}
|
|
|
|
Finally, since the only mutation performed on the list is the \textbf{swap}
|
|
operation at line 22 of the code, and a swap operation does not create or
|
|
destroy values (either it swaps the position of two values or it swaps the same
|
|
position with itself -- i.e. doing nothing), the order-indifferent equality
|
|
predicate can be simply added to this loop as an invariant
|
|
|
|
\begin{minted}{dafny}
|
|
invariant sameElements(a[..], old(a[..]))
|
|
\end{minted}
|
|
|
|
However trivial of a fact as it is, Dafny requires it as an invariant to
|
|
complete the proof of correctness, and therefore we need to be a little redundant.
|
|
|
|
\subsection{Inner loop variant and invariant}
|
|
|
|
The inner loop implements the \textit{arg min} expression used in the assignment
|
|
at line 6 of the pseudocode. From this fact we can easily say this loop does not
|
|
mutate $a$ in any array and therefore the order-indifferent equality predicate
|
|
holds:
|
|
|
|
\begin{minted}{dafny}
|
|
invariant sameElements(a[..], old(a[..]))
|
|
\end{minted}
|
|
|
|
Then, we can define the invariant for the index $i$, which iterates
|
|
over the values in $[s + 1, |a|]$ in single increasing steps. We also know that
|
|
the loop condition is based on the upper bound of this interfal, so we can
|
|
define the loop variant as well:
|
|
|
|
\begin{minted}{dafny}
|
|
invariant s + 1 <= i <= a.Length
|
|
decreases a.Length - i
|
|
\end{minted}
|
|
|
|
The only assignments to variable \textit{min} are at line 11 and line 17 of the
|
|
pseudocode, where \textit{min} is initialized to $s$ and \textit{min} is
|
|
assigned the value of $i$ respectively. Therefore we can say the value of
|
|
\textit{min} at any point where is in scope is either $s$ or $\in [s + 1,|a|)$
|
|
as it is assigned a possible value of $i$ \textit{inside} the loop. We can
|
|
formalize this fact with an invariant:
|
|
|
|
\begin{minted}{dafny}
|
|
invariant s <= min < a.Length
|
|
\end{minted}
|
|
|
|
Finally % it's here for you, it's the last member of the DK crew
|
|
we can define a loop invariant for the values of the list element referenced by
|
|
\textit{min}. As the loop scans for values referenced by $i$ less than
|
|
\mintinline{dafny}{a[min]}, updating \textit{min} with the value of $i$ when
|
|
this is true, we can say that for all values smaller than $i$ in the scanned
|
|
region \mintinline{dafny}{a[min]} indeed contains the smallest value. This fact
|
|
in predicate form results in the following loop invariant:
|
|
|
|
\begin{minted}{dafny}
|
|
invariant forall j: int :: s <= j < i ==> a[min] <= a[j]
|
|
\end{minted}
|
|
|
|
\subsection{Dafny implementation with specification}
|
|
The Dafny implementation of selection sort complete with the specification
|
|
explained so far can be found in the file \texttt{selectionsort.dfy} found in
|
|
the repository:
|
|
|
|
\begin{center}
|
|
\href{https://gitlab.com/usi-si-teaching/msde/2022-2023/software-analysis/maggioni/assigment-1}{gitlab.com:usi-si-teaching/msde/2022-2023/software-analysis/maggioni/assigment-1}
|
|
\end{center}
|
|
|
|
on the \textit{main} branch.
|
|
|
|
\section{Conclusions}
|
|
|
|
Writing specifications with Dafny turned out to indeed be a challenge. Choosing
|
|
the right predicates and the right places to put them to satisfy Danfy and
|
|
Boogie, its embedded theorem prover, was an iterative process requiring many
|
|
attempts and careful scrutiny at the reported errors.
|
|
|
|
As part of this process, I have introduced many \mintinline{dafny}{assert} and
|
|
\mintinline{dafny}{assume} clauses to tackle the algorithm portion by portion.
|
|
As \mintinline{dafny}{assume}s are basically ``cheats'' w.r.t. the correctness
|
|
proving process and \mintinline{dafny}{assert}s were redundant, no such
|
|
statement survives in my implementation.
|
|
|
|
Lines 3-5 of the algorithm's implementation (a simple check of the list $a$
|
|
being empty, and an immediate \mintinline{dafny}{return} if this is the case)
|
|
are not strictly needed according to the pseudocode. However, handling this edge
|
|
case specifically simplifies somewhat the process of determining
|
|
the loop invariants as we can assume in all further statements that the list is
|
|
non-empty.
|
|
|
|
Indeed, the hardest step in the verification process was determining appropriate
|
|
loop invariants to satisfy the theorem proven. The need for redundant
|
|
order-indifferent equality predicates in both loops is quite counter-intuitive
|
|
as those invariants merely re-state a property that is true across the method.
|
|
|
|
\end{document}
|
|
|