report done, 1st submission

README.md

@@ -1,5 +1,5 @@
 # Assignment 1 -- Software Analysis
 
-Dafny *pygments* lexer stored in `pygmentize.py` directory thanks to:
+Dafny *pygments* lexer stored in `pygmentize.py` implemented by:
 
 https://github.com/Locke/pygments-dafny/

report.tex

@@ -66,10 +66,13 @@ Assignment 1 -- Software Analysis \\\vspace{0.5cm}
 
 \begin{document}
 \maketitle
-\tableofcontents
 
 \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
@@ -86,10 +89,6 @@ in algorithm \ref{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|$}
@@ -154,7 +153,7 @@ 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.
+at line 3 of the pseudocode.
 
 \section{Verification}
 
@@ -282,21 +281,62 @@ decreases a.Length - i
 
 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.
+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}
 
-{\color{red}TBD}
+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}  
 
-\begin{verbatim}
-Did you introduce some that you then realized were not needed?
+\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:
 
-Any details of the algorithm’s implementation that you may have had to adjust to
-make specification or verification easier.
- > if list is empty
+\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}
 
-What were the hardest steps of the verification process?
-\end{verbatim}
+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}