
\documentclass[9pt,xcolor=dvipsnames,unknownkeysallowed]{beamer}
%\documentclass[handout,9pt,xcolor=dvipsnames,unknownkeysallowed]{beamer}

\input{../Common/common}



\subtitle{Lecture 3: Programming as a model-based activity}
\date {MRH 19/09/2024}



\begin{document}

\begin{frame}
  \titlepage


\end{frame}


\begin{frame}{Overview}

\begin{itemize}
\item Syntax, semantics and pragmatics (briefly) 
\begin{itemize}
\item Overview of F\#	
\item Semantics of a function declaration 
\end{itemize}

\medskip

\item Programming as a modelling activity
\begin{itemize}
	\item Type declarations (type abbreviations)
	\item Cash register
	\item Map colouring
\end{itemize}
%\ \hfill {\darkgreen Exploiting functional decomposition}

\medskip

\item Program properties and property-based testing


\end{itemize}
\end{frame}




\begin{frame}

\begin{center}
	\huge\darkgreen Syntax, semantics and pragmatics 
\end{center}
\end{frame}





\begin{frame}{Programming languages: Syntax, Semantics and Pragmatics}

\begin{itemize}
	\item The {\blue syntax} is concerned with the (notationally correct) grammatical structure of programs. 
	
	\bigskip
	
	\item<2-> The {\blue semantics} is concerned with the meaning of syntactically correct programs.
	
	
	\bigskip
	
	\item<3-> The {\blue pragmatics} is concerned with practical (adequate) application of language constructs in order to achieve certain objectives. 
\end{itemize}


\bigskip
\pause[4]

A specification of F\# is found at {\darkgreen \url{https://fsharp.org/specs/language-spec/}}
\end{frame}


\begin{frame}
\frametitle{Further characteristics for the functional fragment of F\#}


F\# is a {\redbrown statically typed, compiled language} language:

\bigskip

\begin{itemize}
	
	\item<2-> {\blue At compile time:} A type for every expression in a program is {\darkgreen inferred}. 
	
	If this is not possible, then an type error is issued at compile time 
	%and no code is generated. 
	
	\bigskip
	
	\item<3-> Code is only generated by the compiler for {\redbrown well-typed} programs.
	
	\bigskip
	
	\item<4-> {\blue At runtime:} The generated code contains no type information
	\\ \hfill {\darkgreen well-typed programs do not go wrong} 
	
\end{itemize}

\end{frame}


\begin{frame}

\begin{tabular}{l|l|l}
Syntax   & Static semantics & Semantics \\
& Type inference $\blue e:\tau$    &           \\
\hline 
Types $\blue \tau$    &           &   Value $\blue v$         \\ 
%constants $c$ & $c:\tau$        & Values $c$\\
%Identifiers    & & \\
Patterns $\blue pat$      & &  Binding $\blue id \mapsto v$\\
Expressions  $\blue e$  & Types every piece of an expression & Environment\\
Declarations $\blue d$  & Types every piece of a declaration  & $\blue e_1 \leadsto e_2$ \\
\hline 
indentation  & & \\
\qquad sensitive & & \\

\end{tabular} 

\bigskip

Pragmatics: {\redbrown ?}
\pause

\begin{itemize}
\item {\redbrown type and function names are descriptive}
\item {\redbrown types start with a capital letter}
\item {\redbrown variables names are short and consistently used}
\item {\redbrown function types are stated in comments}
\item a program is composed by small, well-understood pieces
\item adequate use of language constructs
\item ...
\item common computer-science sense
\end{itemize}



\end{frame}




\begin{frame}[fragile]{Overview: Syntactical constructs in ``our part of'' F\# }

\begin{itemize}
	\item Constants: {\blue 0, 1.1, true, ...}
	
	\medskip
	
	\item<2-> Patterns: $\blue x \quad \_  \quad (p_1, \ldots, p_n) \quad p_1\!::\!p_2 \quad [p_1; \ldots; p_n]$\\ 
	$\blue p_1 | p_2 \quad p\ \mathtt{when}\ e \quad p\ \mathtt{as}\ x \quad  p\!:\!t  \ldots$   
	
	\medskip
	
	\item<3-> Expressions: $\blue x \quad (e_1,\ldots,e_n) \quad e_1\!::\!e_2 \quad [p_1; \ldots; p_n] $\\[2mm]
	$\blue e_1 e_2 \quad  e_1\! \oplus\! e_2 \quad (\oplus) \quad \mathtt{let}\ p_1 = e_1\ \mathtt{in}\ e_2$ \\[2mm]
	$\blue  e\!:\!t \quad  \mathtt{if}\ e\ \mathtt{then}\ e_1\  \mathtt{then}\ e_2 \qquad \mathtt{match}\ e\ \mathtt{with}\ clauses$\\[2mm] 
	$\blue \mathtt{fun}\ p_1 \cdots p_n \verb!->! e \qquad \mathtt{function}\ clauses \quad \ldots$   
	
	\medskip
	
	\item<4-> Declarations $\redbrown \mathtt{let}\ f\  p_1 \ldots p_n = e \quad \mathtt{let\ rec}\ f\  p_1 \ldots p_n = e$, \hfill $\blue n\ge 0$  
	
	\medskip
	
	\item<5-> Types\\ $\blue \mathtt{int}  \quad \blue \mathtt{float}  \quad \mathtt{bool}  \quad \mathtt{string}  \quad 'a \quad  {\redbrown T\texttt{<}t_1, \ldots , t_n \texttt{>}} \quad \ldots$\\
	$\blue t_1\!*\!t_2\!*\!\cdots\!*\!t_n  \quad  t\ \mathtt{list}  \quad t_1 \verb|->| t_2 \ldots$  
	
\medskip
	
	\item<6-> Type abbreviations $\blue \mathtt{type}\ T = t \qquad{\redbrown \mathtt{type}\  T\texttt{<}'a_1,\ldots, 'a_n\texttt{>} = t}$
	
\medskip	
	
\item<7-> Type declarations	
	$\blue \mathtt{type}\ T = C_1\ |\ \cdots  |\ C_i\ \texttt{of}\ t_i\ |\ \cdots$
\end{itemize}

\medskip

\onslide<3->{where the construct $\blue clauses$ has the form:
	\begin{alltt}\blue 
		| p\(\sb{1}\) -> e\(\sb{1}\)
		| \(\ldots\)
		| p\(\sb{n}\) -> e\(\sb{n}\)
	\end{alltt} 
}
\end{frame}


\begin{frame}[fragile]\frametitle{What is the value of $\redbrown a$?}

Consider
\begin{alltt}\blue
	
let pi = 3.14;;
	
	
let ca r = pi * r * r;;
	
	
let a = let pi = 1.0;;        
        ca 1.0;; 
	
{\redbrown a?}
	
\end{alltt}


\end{frame}


\begin{frame}[fragile]\frametitle{Semantics of a function: A {\redbrown closure}}

Consider a declaration of $\blue\verb|f|$ in an environment
\qquad $\darkgreen env = [a \mapsto 4, b \mapsto true]$:
\begin{alltt}\blue
   let f x = x+a
\end{alltt}
\pause
The resulting environment is:
\[\darkgreen
[a \mapsto 4, b \mapsto true, f \mapsto cl_f]
\]
\bigskip\pause
where the {\em value of} $\blue f$ is a {\redbrown closure} $\darkgreen cl_f$ =
\[\redbrown 
([x], x+a, [a \mapsto 4])
\]
consisting of 
\begin{itemize}
	\item the argument list: {\redbrown [x]}
	\item the body of f:  {\redbrown x+a}
	\item the environment with bindings for the {\em free} variables: {\redbrown $[a \mapsto 4]$} 
\end{itemize}

\pause\bigskip

The bindings in a closure's environment are determined at the place where the function is declared \hfill {\darkgreen static binding}

\end{frame}


\begin{frame}[fragile]{Function application}
	
Let $\darkgreen env$ be an environment, where the closure for $\blue f$ is 	
\[ \darkgreen cl_{\blue f} = {\blue ([x], e,  env_f)}  \]

\pause 
\bigskip
The application $\blue f(a)$ is evaluated as follows in $\darkgreen env$:
\[\blue
\begin{array}{lcl}
 & & (f(a),{\darkgreen env})\\
\leadsto & & (e, [x \mapsto v] + env_f)
\end{array}	
\] 	
\pause[3]
where 
\begin{itemize}
	\item<3-> $\blue v$ is the value of $\blue a$ in $\darkgreen env$ 
	\item<4-> $\blue [x \mapsto v] + env_f$ is the environment obtained by adding the binding from $\blue x \mapsto v$ to  $\blue env_f$.
\end{itemize} 
\end{frame}


\begin{frame}[fragile]\frametitle{Static binding: an example}

Consider
\begin{alltt}\blue
	
let pi = 3.14;;

                            {\darkgreen env1 = ?}

let ca r = pi * r * r;;

                            {\darkgreen env2 = ?}


let a = let pi = 1.0        
                            {\darkgreen env3 = ?}

        ca 1.0;; 
	
                            {\darkgreen env4 = ?}
                            {\redbrown a?}

\end{alltt}


\end{frame}









\begin{frame}

\begin{center}
	\huge\darkgreen  Programming as a modelling activity
\end{center}
\end{frame}



\begin{frame}{Goal and approach}

Goal: the main concepts of the problem formulation are traceable
in the program.

\bigskip
\pause

Approach: to name the important concepts of the problem and
associate types with the names.
\begin{itemize}
\item This model should facilitate discussions about whether it
fits the problem formulation.
\end{itemize}

\bigskip
\pause

Aim: A succinct, elegant program reflecting the model.

\end{frame}

\begin{frame}{The problem}
\begin{quote}
An electronic cash register contains a data {\darkgreen register}
associating the {\darkgreen name} of the {\darkgreen article} and
its {\darkgreen price} to each valid {\darkgreen article code}. A
{\darkgreen purchase} comprises a {\darkgreen sequence of items},
where each {\darkgreen item} describes the purchase of one or
several pieces of a specific article.

\bigskip
\pause

The task is to construct a program which makes a {\darkgreen bill}
of a purchase. For each item the bill must contain the name of the
article, the {\darkgreen number of pieces}, and the {\darkgreen
total price}, and the bill must also contain the {\darkgreen grand
total} of the entire purchase.
\end{quote}

\end{frame}


\begin{frame}[fragile]\frametitle{A Functional Model}

\begin{itemize}
\item Name key concepts and give them a type
\end{itemize}

\pause

A signature for the cash register:

\begin{center}\small
\begin{tabular}{|l|}
\hline
\verb/type ArticleCode = string/ \\
\verb/type ArticleName = string/ \\
\verb/type Price       = int/  \\
\verb/type Register    = (ArticleCode * (ArticleName*Price)) list/ \\
\verb/type NoPieces    = int/   \\
\verb/type Item        = NoPieces * ArticleCode/ \\
\verb/type Purchase    = Item list/ \\
\verb/type Info        = NoPieces * ArticleName * Price/ \\
\verb/type Infoseq     = Info list/ \\
\verb/type Bill        = Infoseq * Price/ \\
\\
\verb/makeBill: Register -> Purchase -> Bill/ \\

\hline
\end{tabular}
\end{center}

\pause\medskip

\begin{center}\redbrown
Is the model adequate?
\end{center}
\end{frame}

\begin{frame}[fragile]\frametitle{Example}

The following declaration names a register:
\begin{alltt}
let reg = [("a1",("cheese",25));
           ("a2",("herring",4));
           ("a3",("soft drink",5)) ];;
\end{alltt}

\pause
\medskip

The following declaration names a purchase:
\begin{alltt}
let pur = [(3,"a2"); (1,"a1")];;
\end{alltt}

\pause
\medskip

A bill is computed as follows:
\begin{alltt}
makeBill reg pur;;
\ett{val it : (int * string * int) list * int =}
\ett{  ([(3, "herring", 12); (1, "cheese", 25)], 37)}
\end{alltt}
\end{frame}

\begin{frame}[fragile]\frametitle{Functional decomposition (1)}

Type: {\redbrown findArticle: ArticleCode $\to$ Register $\to$ ArticleName * Price}

\begin{alltt}
let rec findArticle ac = function
    | (ac',adesc)::_ when ac=ac' -> adesc
    | _::reg                     -> findArticle ac reg
    | _                          ->
          {\blue failwith(ac + " is an unknown article code")};;
\ett{val findArticle : string -> (string * 'a) list -> 'a}
\end{alltt}
Note that the specified type is an instance of the inferred type.

\pause
\bigskip

An article description is found as follows:
\begin{alltt}
findArticle "a2" reg;;
\ett{val it : string * int = ("herring", 4)}

findArticle "a5" reg;;
\ett{System.Exception: a5 is an unknown article code}
\ett{   at FSI_0016.findArticle[a] ... }
\end{alltt}
Note: {\blue failwith} is a built-in function that raises an exception

\end{frame}


\begin{frame}[fragile]\frametitle{Functional decomposition (2)}

{\blue Type: {\redbrown makeBill: Register $\to$ Purchase $\to$ Bill}}
\begin{alltt}
let rec makeBill reg = function
    | []           -> ([],0)
    | (np,ac)::pur ->
         let (aname,aprice) = findArticle ac reg
         let tprice         = np*aprice
         let (billtl,sumtl) = makeBill reg pur
         ((np,aname,tprice)::billtl, tprice+sumtl);;
\end{alltt}

\medskip
\pause
The specified type is an instance of the inferred type:
\begin{alltt}\blue
\ett{val makeBill :}
\ett{    (string * ('a * int)) list -> (int * string) list}
\ett{                -> (int * 'a * int) list * int}
\end{alltt}

\medskip
\pause

\begin{alltt}
makeBill reg pur;;
\ett{val it : (int * string * int) list * int =}
\ett{  ([(3, "herring", 12); (1, "cheese", 25)], 37)}


\end{alltt}

\end{frame}


\begin{frame}{Summary}

\begin{itemize}
\item A succinct model is achieved using type declarations.

\item<2-> Easy to check whether it fits the problem.

\item<3-> Conscious choice of variables (on the basis of the
model) increases readability of the program.

\item<4-> Standard recursions over lists solve the problem.
\end{itemize}

\end{frame}



\begin{frame}{Example: Map Coloring.}

{\redbrown Color a map so that neighbouring countries
get different colors}

\bigskip

{\setlength{\unitlength}{.5\unitlength}
\begin{center}
{\small
\begin{picture}(140,80)(0,15)

\put(0,30){\framebox(40,40)}

\put(20,50){\makebox(0,0){\tt "b"}}

\put(40,20){\framebox(40,40)}

\put(60,40){\makebox(0,0){\tt "a"}}

\put(80,40){\framebox(40,40)}

\put(100,60){\makebox(0,0){\tt "d"}}

\put(100,0){\framebox(40,40)}

\put(120,20){\makebox(0,0){\tt "c"}}

\end{picture}
}
\end{center}
}

\bigskip

\onslide<2->{The types for country and map:}
\begin{itemize}

\item<2-> We shall consider different types for countries, so we use a type variable , say \texttt{\blue 'c} \\[2mm]
\onslide<3->{Symbols: {\darkgreen c, c1, c2, c'};\ \ Examples:
"a", "b", $\ldots$}

\medskip

\item<4-> The type for \texttt{\blue Map} is polymorphic:\\ 
\texttt{\blue type Map<'c> = ('c * 'c) list} \\[2mm]
\onslide<5->{Symbols: {\darkgreen m};\ \ Example: exMap =
[("a","b"); ("c","d"); ("d","a")]}

\end{itemize}

\pause[5]
\begin{center}\redbrown
How many ways could above map be colored?
\end{center}
\end{frame}

\begin{frame}[fragile]\frametitle{Abstract models for color and coloring}

\begin{itemize}
\item<1->
\texttt{\blue type Color<'c>            = 'c list}\\[2mm]
\onslide<2->{Symbols: {\darkgreen col};\ \ Example: ["c"; "a"]}

\medskip

\item<3->
\texttt{\blue type Coloring<'c>         = Color<'c> list}\\[2mm]
\onslide<4->{Symbols: {\darkgreen cols};\ \ Example: [["c"; "a"];
["b"; "d"]]}
\end{itemize}
\ \hfill \onslide<1->{\em\redbrown Be conscious about symbols and
examples}

\pause[5]
\medskip
{\blue
\begin{alltt}
   colMap:  Map<'c> -> Coloring<'c>
\end{alltt}
}

\pause[6]

\begin{figure}[h]
{\small
\begin{tabular}{@{}l@{}|@{}l@{}|@{}l@{}}
%\ \ \ \ \ \ \ \ \ \ \
 \textbf{Meta symbol: Type\ }  & \textbf{\ Definition} & \textbf{Sample value}\\ \hline
%\cline{2-4}
 \verb/c/ \ \ \qquad country &  \verb/'c/
   & \verb/"a"/  \\
 \verb/m:    Map<'c>/ & \verb/('c * 'c) list/
  & \verb/[("a","b"),("c","d"),("d","a")]/ \\
 \verb/col:  Color<'c>/ &  \verb/'c list/
  & \verb/["a","c"]/ \\
 \verb/cols: Coloring<'c>/ & \verb/Color<'c> list/
  & \verb/[["a","c"],["b","d"]]/ \\
\end{tabular}}
\caption{\label{DataModelFigure} A Data model for map coloring problem}
\end{figure}
\end{frame}



\begin{frame}[fragile]\frametitle{Algorithmic idea}

{\setlength{\unitlength}{.5\unitlength}
\begin{center}
{\small
\begin{picture}(140,80)(0,15)

\put(0,30){\framebox(40,40)}

\put(20,50){\makebox(0,0){\tt "b"}}

\put(40,20){\framebox(40,40)}

\put(60,40){\makebox(0,0){\tt "a"}}

\put(80,40){\framebox(40,40)}

\put(100,60){\makebox(0,0){\tt "d"}}

\put(100,0){\framebox(40,40)}

\put(120,20){\makebox(0,0){\tt "c"}}

\end{picture}
}
\end{center}
}

\bigskip

Insert repeatedly countries in a coloring.

\bigskip

\begin{figure}[h]
{\small
\begin{tabular}{@{}l|c|l|l@{}}
 & country & old coloring & new coloring \\ \hline
1.   & \texttt{"a"} & \verb+[]+      & \verb+[["a"]]+\\
2.   & \texttt{"b"} & \verb+[["a"]]+ & \verb+[["a"] ; ["b"]]+\\
3.   & \texttt{"c"} & \verb+[["a"] ; ["b"]]+ & \verb+[["a";"c"] ; ["b"]]+\\
4.   & \texttt{"d"} & \verb+[["a";"c"] ; ["b"]]+ &
          \verb+[["a";"c"] ; ["b";"d"]]+
\end{tabular}
}
\caption{\label{Idea}Algorithmic idea}
\end{figure}

\end{frame}

\begin{frame}[fragile]\frametitle{Functional decomposition (I)}

\ \hfill {\darkgreen To make things easy}\\

\pause
Are two countries neighbours?

\begin{alltt} \redbrown 
areNb: Map<'c> -> 'c -> 'c -> bool
\end{alltt}


\begin{alltt}\blue
let areNb m c1 c2 ={\redbrown List.contains} (c1,c2) m 
                    ||{\redbrown List.contains} (c2,c1) m;;
\end{alltt}


\pause
\bigskip

Can a color be extended?
\begin{alltt} \redbrown
canBeExtBy: Map<'c> -> Color<'c> -> 'c -> bool
\end{alltt}

\pause
{\blue
\begin{alltt}
let rec canBeExtBy m col c =
  match  col with
  | []       -> true
  | c'::col' -> not (areNb m c' c) && canBeExtBy m col' c;;

canBeExtBy exMap ["c"] "a";;
\ett{val it : bool = true}

canBeExtBy exMap ["a"; "c"] "b";;
\ett{val it : bool = false}
\end{alltt}
}

\end{frame}


\begin{frame}[fragile]\frametitle{Functional composition (I)}
\ \hfill {\darkgreen Combining functions make things easy}\\

\pause
Extend a coloring by a country:
\begin{alltt}\redbrown
extColoring: Map<'c> -> Coloring<'c> -> 'c -> Coloring<'c>
\end{alltt}

\bigskip

{\darkgreen
\begin{verbatim}
Examples:
  extColoring exMap [] "a"       =  [["a"]]
  extColoring exMap [["b"]] "a"  =  [["b"] ; ["a"]]
  extColoring exMap [["c"]] "a"  =  [["a"; "c"]]
\end{verbatim}
}

\pause

{\blue
\begin{alltt}
let rec extColoring m cols c =
    match cols with
    | []         -> [[c]]
    | col::cols' -> if canBeExtBy m col c
                    then (c::col)::cols'
                    else col::extColoring m cols' c;;
\end{alltt}
}


\bigskip

\pause
\begin{center}\em\redbrown
Function types, consistent use of symbols, and examples\\
make program easy to comprehend
\end{center}

\end{frame}




\begin{frame}[fragile]\frametitle{Functional decomposition (II)}

To color a neighbour relation:
\begin{itemize}
\item Get a list of countries from the neighbour relation.

\item Color these countries
\end{itemize}

\bigskip
\pause[2]
Get a list of countries {\redbrown without duplicates}:
{\blue
\begin{verbatim}
let addElem x ys = if List.contains x ys then ys else x::ys;;

let rec countries = function
    | []           -> []
    | (c1,c2)::m -> addElem c1 (addElem c2 (countries m));;
\end{verbatim}
}

\pause[3]

Color a country list:
{\blue
\begin{verbatim}
let rec colCntrs m = function
    | []    -> []
    | c::cs -> extColoring m (colCntrs m cs) c;;
\end{verbatim}
}

\end{frame}


\begin{frame}[fragile]\frametitle{Functional composition (III)}

\begin{center}
The problem can now be solved by\\
\darkgreen combining {\redbrown well-understood pieces}
\end{center}

\pause
\bigskip
Create a coloring from a neighbour relation:
\begin{alltt}\blue
colMap:  Map<'c> -> Coloring<'c>
\end{alltt}

\pause
\bigskip

{\blue
\begin{alltt}
let colMap m = colCntrs m (countries m);;

colMap exMap;;
\ett{val it : string list list = [["c"; "a"]; ["b"; "d"]]}
\end{alltt}
}

\end{frame}



\begin{frame}{On modelling and problem solving}

\begin{itemize}
\item Types are useful in the specification of concepts and
operations.

\item<2-> Conscious and consistent use of symbols enhances
readability.

\item<3->Examples may help understanding the problem and its
solution.

\item<4->Functional paradigm is powerful.

\medskip

\begin{center}\darkgreen 
Problem solving by
combination of well-understood pieces
\end{center}

\end{itemize}

\bigskip
\pause[5]

\begin{center}\redbrown These points are not programming language
specific
\end{center}
\end{frame}


\begin{frame}

\begin{center}
	\huge\darkgreen  Program properties\\ and\\ property-based testing
\end{center}
\end{frame}


\begin{frame}[fragile]\frametitle{Invariant preservation by example}

An integer list {\blue $[x_0; x_1; \ldots ;x_{n-1}]$} is {\darkgreen ordered} if
\[\blue 
x_0 \le x_1\le \cdots \le x_{n-1} \quad \mbox{where $\blue n\ge 0$} \]
\pause 
The  function:
\begin{alltt}\blue
	let rec insert y xs = 
	  match xs with 
	  | []             -> [y]               (* C1 *)
	  | x::_ when y<=x -> y::xs             (* C2 *)
	  | x::rest        -> x::insert y rest  (* C3 *)
\end{alltt}
inserting $\blue y$ in an ordered list $\blue xs$ should satisfy the property:

\medskip

\qquad If $\blue xs$ is ordered,\\ 
\qquad then $\blue \verb|insert|\ y\ xs$ is ordered as well. 

\bigskip
\pause

We say that $\blue\verb|insert|\ y$ respects (or preserves) the {\darkgreen invariant}:
\begin{itemize}
\item if the argument $\blue xs$ is ordered\\
then the value   $\blue \verb|insert|\ y\ xs$ is ordered as well
\end{itemize}

\bigskip
\pause
Function $\blue f$ preserves invariant $\blue p$: 
\begin{itemize}
 	\item if argument $\blue a$ satisfies property $\blue p$, i.e. $\blue p(a)$ holds,\\  then the result $\blue f(a)$ satisfies $\blue p$ as well, i.e. $\blue p(f(a))$ holds
\end{itemize}
 


\end{frame}


\begin{frame}[fragile]
\frametitle{Property-based testing}


{\darkgreen {\em QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs}, Claessen and Hughes, 2000} 


\begin{itemize}
	\item Random generation of values of arbitrary types
	\item Properties are expressed as Boolean-valued functions
\end{itemize}

%\bigskip

\begin{alltt}\blue 
   let rec sort xs = .....
   let rec ordered xs = ... 
	
   // Test that: for all lists xs: ordered(sort xs)
   let sortProp (xs: int list) = ordered(sort xs)
	
   let _ = Check.Quick sortProp
   \ett{\redbrown Ok, passed 100 tests.}
\end{alltt}

The tool has been ported to many languages. We look at {\blue FsCheck} for the .Net platform. Consult 

\begin{itemize}
	\item \url{https://fscheck.github.io/FsCheck/} and 
	\item TipsTricksPrograms	\hfill {\darkgreen DTU Learn}
\end{itemize}

\end{frame}

\begin{frame}[fragile]
\frametitle{Testing for correctness wrt. a reference model (I)}

\begin{alltt}\blue 
   #r "nuget: FsCheck"
   open FsCheck

   let rec sumA xs acc = 
      match xs with
      | []    -> 0
      | x::xs -> sumA xs (x+acc);;   
\end{alltt}

Correctness property wrt.\ the built-in function: List.sum: 
\begin{center}\darkgreen 
for all xs: List.sum xs = sumA xs 0
\end{center}
\pause
\begin{alltt}\blue 
   let sumRefProp xs = List.sum xs = sumA xs 0;;
   let _ = Check.Quick sumRefProp;;
   \ett{Falsifiable, after 2 tests (2 shrinks) (StdGen ...... :}
   \ett{Original:}
   \ett{[-2; -1]}
   \ett{Shrunk:}
   \ett{\darkgreen [1]}
\end{alltt}

\begin{itemize}
\item uses built-in generators for lists
\item tool provides a {\darkgreen short counterexample} 
\end{itemize}

\end{frame}


\begin{frame}[fragile]
\frametitle{Testing for correctness wrt. a reference model (II)}

\begin{alltt}\blue 
let rec sumA xs acc = 
   match xs with
   | []    ->{\redbrown acc}
   | x::xs -> sumA xs (x+acc);;   
\end{alltt}

Correctness property wrt.\ the built-in function: List.sum: 
\begin{center}\darkgreen 
for all xs: List.sum xs = sumA xs 0
\end{center}
\pause
\begin{alltt}\blue 
   let sumRefProp xs = List.sum xs = sumA xs 0;;
   let _ = Check.Quick sumRefProp;;
   \ett{\darkgreen Ok, passed 100 tests.}
\end{alltt}

\pause

\begin{itemize}
\item default is 100 random tests
\item can be configured
\end{itemize}

\end{frame}



\begin{frame}[fragile]
\frametitle{Testing for correctness wrt. a reference model (III)}

Test cases are exposed using {\blue Check.Verbose} as follows:
\begin{alltt}\blue 
let sumRefProp xs = List.sum xs = sumA xs 0;;
let _ = Check.Verbose sumRefProp;;	
\darkgreen
0:
[-2]
.....
99:
[-1; 0; -1; -1; 2; 1; -1; 0; 0; 5; -1; 1; -1; 0; 0; -1; 2; -1; -2; 0; 1; 0; -1;
1; -1; 1; -1; 0; -1; -1; -1; -1; 1; -1; 1; 1; 1; 0; -2; 1; 2; -2; 1; 0; 0; -2;
1; 0; -1; 0; -1; -1; -2; 2; 0; 1; -1; -1; 1; 1; 0; 0; -1; 0; 1; 0; 0; 1; 1; 1;
0]
Ok, passed 100 tests.
\end{alltt}
\end{frame}




\begin{frame}[fragile]
\frametitle{Summary}

Property-based testing supports testing at a high level of abstraction
\begin{itemize}
\item Focus is on fundamental properties -- not on concrete test cases

\item You write programs for properties -- not concrete test cases

\item Properties are tested automatically

\item Short counterexamples are found --- when properties are falsified
\end{itemize}

The examples given here are just appetizers.




\end{frame}

\begin{frame}[fragile]\frametitle{Polynomial project: On checking properties}

The list $\blue [a_0; \ldots; a_{n-1}], n \ge 0$ is a {\em legal} representation of 
polynomial $\blue a_0 + a_1 x + a_2 x^2 + \cdots + a_{n-1} x^{n-1}$ 
if $\redbrown n=0$ or $\redbrown a_{n-1} \neq 0$. 
\begin{itemize}
\item The last element of a representation cannot be 0
\item Each polynomial has a {\darkgreen unique representation} 
\end{itemize}


\bigskip
\pause

You should check {\darkgreen invariant properties} like:
\begin{itemize}
\item  For every legal representation $\blue p$: $\blue \verb-isLegal(mulX-\ p \verb-)-$.
\end{itemize}
%using FsCheck.

\bigskip
\pause

The script: $\blue \verb-PolyGenerator.fsx-$ contains a generator:
\begin{itemize}
\item produces only legal representations of polynomials (type \verb|Poly|)
\item having small coefficients and degrees
\end{itemize}

\bigskip
\pause

You do not need to understand the generator. Just use it, like in:

\begin{alltt}\blue
let mulXwrong p = 0::p
let mulXinvWrong ({\redbrown{p:Poly}}) = isLegal(mulXwrong p);;

let testMulXInvWrong = Check.Quick mulXinvWrong;;
\ett{>Falsifiable, after 6 tests (0 shrinks) (StdGen (261...}
\ett{	Original:
	[]}
\end{alltt}	
	







\end{frame}


\end{document}


