diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2fa12f5 --- /dev/null +++ b/.gitignore @@ -0,0 +1,303 @@ +*.dll +*.runtimeconfig.json +## Core latex/pdflatex auxiliary files: +*.aux +*.lof +*.log +*.lot +*.fls +*.out +*.toc +*.fmt +*.fot +*.cb +*.cb2 +.*.lb + +## Intermediate documents: +*.dvi +*.xdv +*-converted-to.* +# these rules might exclude image files for figures etc. +# *.ps +# *.eps +# *.pdf + +## Generated if empty string is given at "Please type another file name for output:" +.pdf + +## Bibliography auxiliary files (bibtex/biblatex/biber): +*.bbl +*.bcf +*.blg +*-blx.aux +*-blx.bib +*.run.xml + +## Build tool auxiliary files: +*.fdb_latexmk +*.synctex +*.synctex(busy) +*.synctex.gz +*.synctex.gz(busy) +*.pdfsync + +## Build tool directories for auxiliary files +# latexrun +latex.out/ + +## Auxiliary and intermediate files from other packages: +# algorithms +*.alg +*.loa + +# achemso +acs-*.bib + +# amsthm +*.thm + +# beamer +*.nav +*.pre +*.snm +*.vrb + +# changes +*.soc + +# comment +*.cut + +# cprotect +*.cpt + +# elsarticle (documentclass of Elsevier journals) +*.spl + +# endnotes +*.ent + +# fixme +*.lox + +# feynmf/feynmp +*.mf +*.mp +*.t[1-9] +*.t[1-9][0-9] +*.tfm + +#(r)(e)ledmac/(r)(e)ledpar +*.end +*.?end +*.[1-9] +*.[1-9][0-9] +*.[1-9][0-9][0-9] +*.[1-9]R +*.[1-9][0-9]R +*.[1-9][0-9][0-9]R +*.eledsec[1-9] +*.eledsec[1-9]R +*.eledsec[1-9][0-9] +*.eledsec[1-9][0-9]R +*.eledsec[1-9][0-9][0-9] +*.eledsec[1-9][0-9][0-9]R + +# glossaries +*.acn +*.acr +*.glg +*.glo +*.gls +*.glsdefs +*.lzo +*.lzs +*.slg +*.slo +*.sls + +# uncomment this for glossaries-extra (will ignore makeindex's style files!) +# *.ist + +# gnuplot +*.gnuplot +*.table + +# gnuplottex +*-gnuplottex-* + +# gregoriotex +*.gaux +*.glog +*.gtex + +# htlatex +*.4ct +*.4tc +*.idv +*.lg +*.trc +*.xref + +# hyperref +*.brf + +# knitr +*-concordance.tex +# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files +# *.tikz +*-tikzDictionary + +# listings +*.lol + +# luatexja-ruby +*.ltjruby + +# makeidx +*.idx +*.ilg +*.ind + +# minitoc +*.maf +*.mlf +*.mlt +*.mtc[0-9]* +*.slf[0-9]* +*.slt[0-9]* +*.stc[0-9]* + +# minted +_minted* +*.pyg + +# morewrites +*.mw + +# newpax +*.newpax + +# nomencl +*.nlg +*.nlo +*.nls + +# pax +*.pax + +# pdfpcnotes +*.pdfpc + +# sagetex +*.sagetex.sage +*.sagetex.py +*.sagetex.scmd + +# scrwfile +*.wrt + +# svg +svg-inkscape/ + +# sympy +*.sout +*.sympy +sympy-plots-for-*.tex/ + +# pdfcomment +*.upa +*.upb + +# pythontex +*.pytxcode +pythontex-files-*/ + +# tcolorbox +*.listing + +# thmtools +*.loe + +# TikZ & PGF +*.dpth +*.md5 +*.auxlock + +# titletoc +*.ptc + +# todonotes +*.tdo + +# vhistory +*.hst +*.ver + +# easy-todo +*.lod + +# xcolor +*.xcp + +# xmpincl +*.xmpi + +# xindy +*.xdy + +# xypic precompiled matrices and outlines +*.xyc +*.xyd + +# endfloat +*.ttt +*.fff + +# Latexian +TSWLatexianTemp* + +## Editors: +# WinEdt +*.bak +*.sav + +# Texpad +.texpadtmp + +# LyX +*.lyx~ + +# Kile +*.backup + +# gummi +.*.swp + +# KBibTeX +*~[0-9]* + +# TeXnicCenter +*.tps + +# auto folder when using emacs and auctex +./auto/* +*.el + +# expex forward references with \gathertags +*-tags.tex + +# standalone packages +*.sta + +# Makeindex log files +*.lpz + +# xwatermark package +*.xwm + +# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib +# option is specified. Footnotes are the stored in a file with suffix Notes.bib. +# Uncomment the next line to have this generated file ignored. +#*Notes.bib \ No newline at end of file diff --git a/README.md b/README.md index e69de29..da7f338 100644 --- a/README.md +++ b/README.md @@ -0,0 +1,5 @@ +# Assignment 1 -- Software Analysis + +Dafny *pygments* lexer stored in `pygmentize.py` directory thanks to: + +https://github.com/Locke/pygments-dafny/ diff --git a/pygmentize.py b/pygmentize.py new file mode 100755 index 0000000..e9ac9fd --- /dev/null +++ b/pygmentize.py @@ -0,0 +1,91 @@ +# -*- coding: utf-8 -*- +#!/usr/bin/env python3 +""" + pygments.lexers.dafny + ~~~~~~~~~~~~~~~~~~~~~~~~~~ + + Lexers for Dafny. + + :copyright: Copyright 2006-2022 by the Pygments team, see AUTHORS. + :license: BSD, see LICENSE for details. +""" + +import re + +from pygments.lexer import RegexLexer, include, bygroups +from pygments.token import * + +import argparse +import sys +import pygments.cmdline as _cmdline +import pygments.lexer as _lexer +import pygments.token as _token + + +def main(args): + parser = argparse.ArgumentParser() + parser.add_argument('-l', dest='lexer', type=str) + opts, rest = parser.parse_known_args(args[1:]) + if opts.lexer == 'dafny': + args = [__file__, '-l', __file__ + ':DafnyLexer', '-x', *rest] + _cmdline.main(args) + + +class DafnyLexer(RegexLexer): + """ + For Dafny source code. + """ + + name = 'Dafny' + aliases = ['dafny'] + filenames = ['*.dfy'] + mimetypes = [] + + flags = re.DOTALL | re.UNICODE | re.MULTILINE + + valid_name = r'[\w_]+' + + tokens = { + 'commentsandwhitespace': [ + (r'\s+', Text), + (r'//.*?\n', Comment.Single), + (r'/\*.*?\*/', Comment.Multiline), + ], + 'string': [ + (r'"(\\\\|\\"|[^"])*"', String.Double), + (r"'(\\\\|\\'|[^'])*'", String.Single), + ], + 'root': [ + include('commentsandwhitespace'), + (r'(:=)', Operator), + (r'(\|)', Operator), + (r'(;|::|:|\.\.|`)', Punctuation), + (r'[{(\[,.\])}]', Punctuation), + (r'(==|!=|<=|>=|=|&&|[-<>+*/%])', Operator), + (r'(in)\b', Operator), + (r'(this|old|print)\b', Name.Function.Magic), + (r'(multiset)(\s*)(\()', bygroups(Name.Function.Magic, Text, Punctuation)), + (r'(reads|modifies|ensures|requires|assert|assume|expect|invariant|decreases|constructor)\b', Keyword), + (r'(if|then|else|while|returns|forall)\b', Keyword), + (r'(function|method|predicate|lemma)(\s+\{[^\}]+\}\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Function)), + (r'(function|method|predicate|lemma)(\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Function)), + (r'(function|method|predicate|lemma)', Keyword.Declaration), + (r'(trait|class|datatype)(\s+\{[^\}]+\}\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Class)), + (r'(trait|class|datatype)(\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Class)), + (r'(trait|class|datatype)', Keyword.Declaration), + (r'(extends)(\s+)(\w+)', bygroups(Keyword, Text, Name.Class)), + (r'(extends)', Keyword), + (r'(var)(\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name)), # actually Name.Variable.Instance, but that would be inconsistent, as we don't know this information on other occurrences + (r'(var|ghost)\b', Keyword.Declaration), + (r'(true|false)\b', Keyword.Constant), + (r'(array|seq|set|multiset|int|nat|string|char)\b', Keyword.Type), + (r'[0-9]+', Number.Integer), + include('string'), + + (valid_name, Name), + ] + } + +if __name__ == '__main__': + main(sys.argv) + diff --git a/report.pdf b/report.pdf new file mode 100644 index 0000000..e585de9 Binary files /dev/null and b/report.pdf differ diff --git a/report.tex b/report.tex new file mode 100644 index 0000000..4fa08b1 --- /dev/null +++ b/report.tex @@ -0,0 +1,230 @@ +\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) +{ + 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} 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) +{ + 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, b: seq) +{ + multiset(a) == multiset(b) +} +\end{minted} + +Therefore, the method signature including preconditions and postconditions +is: + +\begin{minted}{dafny} +method SelectionSort(a: array) + 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} + diff --git a/selectionsort.dfy b/selectionsort.dfy index 27ac285..ee453ed 100644 --- a/selectionsort.dfy +++ b/selectionsort.dfy @@ -1,11 +1,17 @@ -predicate sorted(s: seq) { +predicate sorted(s: seq) +{ forall i,j: int :: 0 <= i < j < |s| ==> s[i] <= s[j] } +predicate sameElements(a: seq, b: seq) +{ + multiset(a) == multiset(b) +} + method SelectionSort(a: array) modifies a - ensures sorted(a[..]); - ensures multiset(a[..]) == multiset(old(a[..])); + ensures sorted(a[..]) + ensures sameElements(a[..], old(a[..])) { if (a.Length == 0) { return; @@ -14,7 +20,7 @@ method SelectionSort(a: array) var s := 0; while (s < a.Length - 1) - invariant multiset(a[..]) == multiset(old(a[..])); + invariant sameElements(a[..], old(a[..])) invariant forall i,j: int :: 0 <= i < s <= j < a.Length ==> a[i] <= a[j] invariant s <= a.Length - 1 invariant s >= 1 ==> sorted(a[0..s]) @@ -24,7 +30,7 @@ method SelectionSort(a: array) var i: int := s + 1; while i < a.Length - invariant multiset(a[..]) == multiset(old(a[..])); + invariant sameElements(a[..], old(a[..])) invariant s <= min < a.Length invariant s + 1 <= i <= a.Length invariant forall j: int :: s <= j < i ==> a[min] <= a[j] diff --git a/slowsort.dfy b/slowsort.dfy deleted file mode 100644 index 86a07f9..0000000 --- a/slowsort.dfy +++ /dev/null @@ -1,78 +0,0 @@ -predicate sorted(s: seq) { - forall i,j: int :: 0 <= i < j < |s| ==> s[i] <= s[j] -} - -predicate sameElements(sa: seq, sb: seq) { - multiset(sa) == multiset(sb) -} - -lemma SubSort(s: seq, i: int, j: int) - requires sorted(s) - requires 0 <= i < j <= |s| - ensures sorted(s[i..j]) -{ -} - -method SlowSortHelper(a: array, startIdx: int, endIdx: int) - requires 0 <= startIdx <= endIdx < a.Length - modifies a - ensures a[..startIdx] == old(a[..startIdx]) - ensures endIdx < a.Length ==> a[endIdx + 1..] == old(a[endIdx + 1..]) - ensures sorted(a[startIdx..endIdx + 1]) - ensures multiset(a[startIdx..endIdx + 1]) == multiset(old(a[startIdx..endIdx + 1])) - decreases endIdx - startIdx -{ - if (endIdx == startIdx) { - return; - } - - var middleIdx: int := (startIdx + endIdx) / 2; - assert sameElements(a[startIdx..endIdx + 1], old(a[startIdx..endIdx + 1])); - - SlowSortHelper(a, startIdx, middleIdx); - SlowSortHelper(a, middleIdx + 1, endIdx); - - assert 0 <= startIdx <= middleIdx < endIdx; - assert a[..startIdx] == old(a[..startIdx]); - assert endIdx < a.Length ==> a[endIdx + 1..] == old(a[endIdx + 1..]); - - assert sorted(a[startIdx..middleIdx + 1]); - assert sorted(a[middleIdx + 1..endIdx + 1]); - - if (a[endIdx] < a[middleIdx]) { - a[endIdx], a[middleIdx] := a[middleIdx], a[endIdx]; - } - - assert a[middleIdx] <= a[endIdx]; - assert forall j: int :: startIdx <= j <= endIdx ==> a[j] <= a[endIdx]; - - SlowSortHelper(a, startIdx, endIdx - 1); - - assert 0 <= startIdx <= middleIdx < endIdx; - assert sorted(a[startIdx..endIdx]); - assert multiset(a[startIdx..endIdx]) == multiset(old(a[startIdx..endIdx])); - assert forall j: int :: startIdx <= j <= endIdx ==> old(a[j]) <= a[endIdx]; - - -// assert 0 <= startIdx < middleIdx + 1 <= endIdx; -// assert sorted(a[startIdx..endIdx]); - -// assert a[..startIdx] == old(a[..startIdx]); -// assert endIdx < a.Length ==> a[endIdx + 1..] == old(a[endIdx + 1..]); - -// assert sorted(a[startIdx..endIdx]); -// assert middleIdx <= endIdx ==> a[middleIdx] < a[endIdx]; - -// assert forall j: int :: startIdx <= j < endIdx ==> a[j] <= a[endIdx]; - -} - -method SlowSort(a: array) -modifies a -ensures sorted(a[..]) -ensures sameElements(a[..], old(a[..])) -{ - if (a.Length > 1) { - SlowSortHelper(a, 0, a.Length - 1); - } -} \ No newline at end of file