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

\input{../Common/common}


\usepackage{tikz}
\usetikzlibrary{decorations.pathreplacing}


\title % (optional, use only with long paper titles)
{02157 Functional Programming}

\subtitle
{Lecture: Verification briefly} % (optional)

\date {MRH 25/11/2024}% (optional)
%{Advanced Topics on Embedded Systems}



\begin{document}

\begin{frame}
  \titlepage


\end{frame}



\begin{frame}
	
	
\begin{center}
	\Large\darkgreen 
	You can prove properties of pure functional programs\\[4mm] 
	using ``just''\\[4mm]
	your prerequisites in discrete mathematics
	
\end{center}	
	
	
\end{frame}

\begin{frame}
	
\begin{itemize}
	
\item Unit testing\\
-- {\blue test examples} 
-- a few {\darkgreen sanity checks}  
\bigskip

\item ...

\bigskip

\item Property-based testing\\
-- Validation of {\blue properties of programs}\\ 
-- {\darkgreen Program correctness} supported by {\blue statistical information}


\bigskip


\item ...

\bigskip	


\item Verification\\
-- {\blue properties of program} {\redbrown proved to be correct}\\
-- {\darkgreen Program correctness} guaranteed by {\blue mathematical proofs}
\end{itemize}	
	
\bigskip


	
\end{frame}



\begin{frame}{Pure functional programs}



A simple setting for verification of 
\begin{itemize}
\item {\darkgreen terminating} functional programs \\
\ \hfill {\redbrown excludes, for example,  let rec f(x) = 1+f(x)}\\

\bigskip

\item {\darkgreen having no side-effects}
\end{itemize}

\bigskip

\pause

\bigskip

Reasoning is guided by 
\begin{itemize}
	
\item equations based on program declarations 

\item mathematical properties like {\blue e + e = 2e}

\item induction based on natural numbers and data types

\end{itemize}

\bigskip

\pause

\begin{center}\redbrown
	The simple reasoning breaks down in the presence of side effects, where, for example,
	$\blue e + e = 2e$ does not necessary hold.
\end{center}


\end{frame}


\begin{frame}[fragile]
\frametitle{A very, very simple example: factorial function}

We prove $\blue \forall n\in \Nat.fact\, n = n!$, where

\medskip

{\blue
\begin{alltt}
let rec fact = 
   function
   | 0 -> 1                  (* Case 1 *)
   | n -> n * fact(n-1)      (* Case 2 *)
\end{alltt}
}

\medskip

using the following {\redbrown well-known} induction rule for
natural numbers

\medskip

\begin{tabular}{lll}
1. & $\blue P(0)$ & base case\\
2. & $\blue \forall n.(P(n) \Rightarrow P(n+1))$ & inductive step\\
\hline
   & $\blue \forall n.P(n)$ &
\end{tabular}

\pause

\vspace{-4mm} \ \hfill \mbox{\redbrown What is $\blue P(n)$?}

\medskip
\pause

Base case. We must prove $\blue fact\, 0 = 0! = 1$. Trivial.
\medskip

\pause
Inductive step. Consider arbitrary $\blue n \in \Nat$. We
must establish
\[\blue \underbrace{\underbrace{fact\, n = n!}_{\darkgreen induction\ hypothesis}}_{P(n)} \Rightarrow
\underbrace{fact(n+1) = (n+1)!}_{P(n+1)}\]
\end{frame}



\begin{frame}{Very, very simple example cont'd}

Assume the induction hypothesis:
\[\blue fact\, n = n! \ \ \ \ \ \ \ \ \ (Ind. hyp.)
\]

The inductive step is established by:
\[\blue
\begin{array}{lll}
   & fact(n+1) & \\
 = & (n+1) \cdot fact\, n  & Case\ 2, as\ n+1 \neq 0\\
 = & (n+1) \cdot n!  \ \ \ \ \ \ \ \ \ \ \ \ & Ind. hyp.\\
 = & (n+1)! &
\end{array}
\]

\medskip

\pause
Hence
 $\blue \forall n\in \Nat.fact\, n = n!$ by the induction rule.

\bigskip

\pause

\begin{center}\darkgreen
Simple induction and equational reasoning
\end{center}

\bigskip

\pause

\begin{center}\redbrown
The simple reasoning breaks down in the presence of side effects
\end{center}

\end{frame}





\begin{frame}[fragile]
\frametitle{Structural induction over lists}

The declaration {\blue
\begin{verbatim}
   type 'a list = 
       | Nil                   //        Nil is written []     
       | Cons of 'a * 'a list  // Cons(x,xs) is written x::xs 
\end{verbatim}}
denotes an inductive definition of lists (of type 'a)

\begin{itemize}

\item \mbox{[]}  is a list

\item if $x$ is an element and $xs$ is a list, then $x::xs$ is a
list

\item lists can be generated by above rules only

\end{itemize}

\pause
\bigskip

The following structural induction rule is therefore sound:

\begin{tabular}{lll}
1. & $\blue P([])$ & base case\\
2. & $\blue \forall xs.\forall x.(P(xs) \Rightarrow P(x::xs))$ & inductive step\\
\hline
   & $\blue \forall xs.P(xs)$ &
\end{tabular}

\end{frame}

\begin{frame}[fragile]
	\frametitle{Example}
	
{\blue
\begin{verbatim}
let rec (@) xs ys = match xs with
                    | [] -> ys                   (* A1 *)
                    | x::xs -> x::(xs @ ys);;    (* A2 *)
                    
let rec len xs = match xs with 
                 | [] -> 0                       (* L1 *)
                 | _::xs -> 1+len xs;;           (* L2 *)
\end{verbatim}}



\bigskip\pause

Property:
\begin{center} \blue $ \forall xs. len(xs@ys) = len(xs) + len(ys)$
\end{center}

\end{frame}



\begin{frame}[fragile]
	\frametitle{Proof of property by induction (I)}


	
	We prove: $\blue \forall xs. len(xs@ys) = len(xs) + len(ys)$
	\hfill {\redbrown (1)}
	
	\pause
	\bigskip
	
	Let $\blue P(xs)$ be $\blue len(xs@ys) = len(xs) + len(ys)$
	
	\bigskip
	\pause
	
	Base case: We must establish: $\blue P([\, ])$: 

\pause
\medskip
	
\[\blue  
\begin{array}{lll}
  & len([] @ ys) & \\ 
= & len(ys) & {\darkgreen A1} \\
= & 0 + len(ys) & {\darkgreen Arith.} \\
= & len([]) + len(ys) & {\darkgreen L1}
\end{array}
\]
 
\end{frame}

\begin{frame}[fragile]
	\frametitle{Proof of property by induction (II)}	

Remember: $\blue P(xs)$ is $\blue len(xs@ys) = len(xs) + len(ys)$ \hfill  {\redbrown ind. hyp.}
	
	
	\bigskip
	\pause
	
Inductive step: Consider arbitrary $\blue xs$ and $\blue x$.

\medskip 

Assume $\blue P(xs)$ the {\redbrown induction hypothesis}.

\medskip 

We must establish $\blue P(x::xs)$: 
\[\blue 
len((x::xs) @ ys)) = len(x::xs) + len(ys)
\]

\pause
Simple equational reasoning suffices:

\[\blue  \begin{array}{lll}
	& len((x::xs)@ys) & \\
\onslide<4->{=} & \onslide<4->{len(x::(xs@ys))} & \onslide<4->{\darkgreen A2}\\
	\onslide<5->{=} & \onslide<5->{1+len(xs@ys)}  & \onslide<5->{\darkgreen L2}\\
	\onslide<6->{=} & \onslide<6->{1+(len(xs) + len(ys))} & \onslide<6->{\redbrown ind. hyp.}\\
	\onslide<7->{=} & \onslide<7->{(1+len(xs)) + len(ys)} & \onslide<7->{\darkgreen Arith.}\\
	\onslide<8->{=} & \onslide<8->{len(x::xs) + len(ys)} & \onslide<8->{\darkgreen L2}
\end{array}
\]
\bigskip
	
	\pause[9]
	
Using the structural induction rule we have established 
\begin{center}
 $\blue \forall xs. len(xs@ys) = len(xs) + len(ys)$
\end{center}
	
	
\end{frame}





\begin{frame}[fragile]
\frametitle{Just an appetizer}

Reasoning about functional programs is "easy"
\begin{itemize}
\item no side effects
\item inductively defined types (lists, trees, ...)
\end{itemize}

\pause 
\bigskip


Topics from Program analysis, Model checking and Verification are studied in a variety of courses, e.g.\ 02141, 02143, 02156, 02242, 02244, 02245, 02246 introducing different theories and using highly advanced tools





\end{frame}

\end{document}
