%\documentclass[t,12pt,numbers,fleqn,handout]{beamer}
\documentclass[t,12pt,numbers,fleqn]{beamer}

\usepackage{pgfpages} 
\usepackage{hyperref}
\hypersetup{colorlinks=true,
    linkcolor=blue,
    citecolor=blue,
    filecolor=blue,
    urlcolor=blue,
    unicode=false}
\urlstyle{same}

\usepackage{hhline}
\usepackage{booktabs}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{array}
\usepackage{listings}

\usepackage{amssymb}
\usepackage{amsmath}

\useoutertheme{split} %so the footline can be seen, without needing pgfpages

% \pgfpagesuselayout{resize to}[letterpaper,border
% shrink=5mm,landscape] %if this is uncommented, the hyperref links do not work

\mode<presentation>{}

\input{../def-beamer}

\newcommand{\topic}{29 Introduction to Verification (Ch.\ 6)}

\input{../titlepage}

\begin{document}

\input{../footline}

\lstset{language=java,breaklines=true,showspaces=false,showstringspaces=false,breakatwhitespace=true}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Introduction to Verification}

\begin{itemize}
\item Partially based on slides by Dr.\ Wassyng, Ghezzi et al
\item Administrative details
\item pointInRegion(p)
\item Outline of verification topics
\item Testing so far in SFWR ENG 2AA4
\item Need for verification
\item Properties and approaches to verification
\item Goals of testing
\item Test plan
\item Types of test - white box, versus black box, manual versus automated, etc.
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Administrative Details}

\begin{itemize}

\item Investigating 9 academic integrity cases for A2

\item A3 deadlines
\begin{itemize}
\item Part 2 - Code: due 11:59 pm Mar 20
\item {Part 1 spec available in repo}
\item \structure{Change of $<$ to $\leq$ in natural language and spec}
\end{itemize}

\item A4
\bi
\item Your own design and specification
\item Due April 3 at 11:59 pm
\ei

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{A Table for pointInRegion(p)}

\begin{itemize}

\item Consider all of the cases
\item Draw a picture
\item Short form notation
\begin{itemize}
\item $px = p.\mbox{xcoord()}$
\item $py = p.\mbox{ycoord()}$
\item $llx = \mathit{lower\_left}.\mbox{xcoord()}$
\item $lly = \mathit{lower\_left}.\mbox{ycoord()}$
\item $llxw = \mathit{lower\_left}.\mbox{xcoord()} + \mathit{width}$
\item $llyh = \mathit{lower\_left}.\mbox{ycoord()} + \mathit{height}$
\item T = Constants.TOLERANCE
\end{itemize}

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[plain]
\frametitle{Nine Cases}

\begin{tabular}{|p{2.cm}|p{2.8cm}|p{5.3cm}|}
\hhline{~|~|-|}
\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
\hhline{|-|-|-|}
{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$lly \leq py \leq llyh$} & {$(llx - px) \leq \mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
\hhline{-|-|-|}
{$llx \leq px \leq llxw$} & {$py < lly$} & {$(lly-py) \leq\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$lly \leq py \leq llyh$} & {$\mbox{True}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$(py - llyh) \leq \mbox{T}$}\\
\hhline{-|-|-|}
{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$lly \leq py \leq llyh$} & {$(px-llxw) \leq \mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw,llyh)) \leq \mbox{T}$}\\
\hhline{-|-|-|}

\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Seven Cases}

\begin{tabular}{|p{2.cm}|p{2.8cm}|p{5.3cm}|}
\hhline{~|~|-|}
\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
\hhline{|-|-|-|}
{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$lly \leq py \leq llyh$} & {$(llx - px) \leq \mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
\hhline{|-|-|-|}
\multicolumn{2}{|l|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
\mbox{T})$}\\
\hhline{|-|-|-|}
{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$lly \leq py \leq llyh$} & {$(px-llxw) \leq \mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
\hhline{-|-|-|}

\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Six Cases}

\begin{tabular}{|p{2.5cm}|p{2.5cm}|p{5.1cm}|}
\hhline{~|~|-|}
\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
\hhline{|-|-|-|}
{$px < llx$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llx, lly)) \leq
\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llx, llyh)) \leq \mbox{T}$}\\
\hhline{|-|-|-|}
\multicolumn{2}{|l|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
\mbox{T})$}\\
\hhline{|-|-|-|}
{$px > llxw$} & {$py < lly$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, lly)) \leq
\mbox{T}$}\\
\hhline{|~|-|-|}
~ & {$py > llyh$} & {$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) \leq \mbox{T}$}\\
\hhline{-|-|-|}
\multicolumn{2}{|l|}{{$lly \leq py \leq llyh$}} & {$(llx-\mbox{T}) \leq px \leq (llxw +
\mbox{T})$}\\
\hhline{|-|-|-|}

\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Three Cases}

\begin{tabular}{|p{2.5cm}|p{2.5cm}|p{5.1cm}|}
\hhline{~|~|-|}
\multicolumn{1}{r}{} & \multicolumn{1}{r|}{} & \multicolumn{1}{l|}{\textbf{out}}\\
\hhline{|-|-|-|}
\multicolumn{2}{|p{5cm}|}{{$llx \leq px \leq llxw$}} & {$(lly-\mbox{T}) \leq py \leq (llyh +
\mbox{T})$}\\
\hhline{|-|-|-|}
\multicolumn{2}{|p{5cm}|}{{$lly \leq py \leq llyh$}} & {$(llx-\mbox{T}) \leq px \leq (llxw +
\mbox{T})$}\\
\hhline{|-|-|-|}
\multicolumn{2}{|p{5cm}|}{{$\neg(llx \leq px \leq llxw) \wedge \neg(lly \leq py \leq llyh)$}} &
{$\mbox{min}[p.\mbox{dist}(\mbox{PointT}(llx, lly)),$ $p.\mbox{dist}(\mbox{PointT}(llxw, lly)),$
$p.\mbox{dist}(\mbox{PointT}(llx, llyh)),$ 
$p.\mbox{dist}(\mbox{PointT}(llxw, llyh)) ] \leq \mbox{T}$}\\
\hhline{|-|-|-|}

\end{tabular}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Nine Cases, but 2D}

\bi
\item \structure{How would you write all 9 cases, but with a tabular form that
    closely matches the original 2D problem description?}
\ei

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Outline of Verification Topics}

\begin{itemize}

\item What are the goals of verification?
\item What are the main approaches to verification?
\begin{itemize}
\item What kind of assurance do we get through testing?  
\item \structure{Can testing prove correctness?}
\item How can testing be done systematically?
\item How can we remove defects (debugging)?
\end{itemize}
\item What are the main approaches to software analysis?
\item Informal versus formal analysis

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Testing on Assignment 1 to 3}

\begin{itemize}

\item Limited guidance on test case selection
\item Maybe improved test cases would improve the results?
\item Consider the method for deleting from a sequence of T (next slide)
\item We have been using automated testing
\item We have seen the advantages of regression testing
\item Some have adopted the excellent strategy of testing while developing
\begin{itemize}
\item Helps isolate errors
\item Does not leave testing to the end when there is no time to do it properly
\item Helps improve the understanding of the problem and the program
\end{itemize}
\item Hopefully the experience on the assignments has motivated you to think
  more about testing

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Incorrect Version of Delete}

Using \texttt{s = new T[MAX\_SIZE]}, for some type \texttt{T}

\lstset{language=java,breaklines=true,showspaces=false,showstringspaces=false,breakatwhitespace=true}
\noindent \lstinputlisting{DeleteIncorrect.java}

\bi
\item \structure{What is the error?}
\item \structure{What test case would highlight the error?}
\ei

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Correct Version of Delete}

\lstset{language=java,breaklines=true,showspaces=false,showstringspaces=false,breakatwhitespace=true}
\noindent \lstinputlisting{DeleteCorrect.java}

Avoids potential ArrayIndexOutOfBoundsException Exception

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Verification Versus Validation}

\begin{itemize}

\item \structure{What is the difference between verification and
    validation?}

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Verification Versus Validation}

\begin{itemize}

\item Verification - Are we building the product right?  Are we implementing the
  requirements correctly (internal)
\item Validation - Are we building the right product? Are we getting the right
  requirements (external)
\item According to
  \href{https://en.wikipedia.org/wiki/Software_verification_and_validation}{Capability
    Maturity Model (CMM)}
\bi
\item 
    Software Verification: The process of evaluating software to determine
    whether the products of a given development phase satisfy the conditions
    imposed at the start of that phase. [IEEE-STD-610]
  \item Software Validation: The process of evaluating software during or at the
    end of the development process to determine whether it satisfies specified
    requirements. [IEEE-STD-610] 
\ei
\item We will focus on verification
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Verification Activities}

\begin{center}
\includegraphics[scale=0.55]{../Figures/SoftwareLifecycle.png}
\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}
\frametitle{Need for Verification}

\begin{itemize}

\item Designers are fallible even if they are skilled and follow sound principles
\item We need to build confidence in the software
\item Everything must be verified, every required functionality, every required
  quality, every process, every product, every document
\item For every work product covered in this class we have discussed its verification
\item Even verification itself must be verified

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Properties of Verification}

\begin{itemize}

\item May not be binary (OK, not OK)
\begin{itemize}
\item Severity of defect is important
\item Some defects may be tolerated
\item Our goal is typically acceptable reliability, not correctness
\end{itemize}
\item May be subjective or objective - for instance, usability, generic level of
  maintainability or portability
\bi
\item \structure{How might we make usability objective?}
\ei
\item Even implicit qualities should be verified
\begin{itemize}
\item Because requirements are often incomplete
\item For instance robustness, maintainability
\end{itemize}
\item \structure{What is better than implicitly specified
    qualities?} % explicit!
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Approaches to Verification}

\begin{itemize}

\item \structure{What are some approaches to verification?}
\item \structure{How can we categorize these approaches?}

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
\frametitle{Approaches to Verification}

\begin{itemize}

\item Experiment with behaviour of product
\begin{itemize}
\item Sample behaviours via testing
\item Goal is to find ``counter examples''
\item \structure{Dynamic} technique
\item Examples: unit testing, integration testing, acceptance testing, white box
  testing, stress testing, etc.
\end{itemize}
\item Analyze product to deduce its adequacy
\begin{itemize}
\item Analytic study of properties
\item \structure{Static} technique
\item Examples: Code walk-throughs, code inspections, correctness proof, etc.
\end{itemize}

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}