Skip to content
Snippets Groups Projects
Commit 7d71ed48 authored by W. Spencer Smith's avatar W. Spencer Smith
Browse files

First draft of L29.

parent 4dc594eb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Lectures/L29_IntroductionToVerification/DeleteCorrect.java 0 → 100644
+ 11
− 0
View file @ 7d71ed48
public static void del(int i)
{
int j;
for (j = i; j < (length - 1); j++)
{
s[j] = s[j+1];
}
length = length - 1;
}
\ No newline at end of file
Lectures/L29_IntroductionToVerification/DeleteIncorrect.java 0 → 100644
+ 11
− 0
View file @ 7d71ed48
public static void del(int i)
{
int j;
for (j = i; j <= (length - 1); j++)
{
s[j] = s[j+1];
}
length = length - 1;
}
\ No newline at end of file
Lectures/L29_IntroductionToVerification/IntroductionToVerification.pdf 0 → 100644
+ 0
− 0
View file @ 7d71ed48
File added
Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex 0 → 100755
+ 352
− 0
View file @ 7d71ed48
%\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}
\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 Today's slide are partially based on slides by Dr.\ Wassyng, Ghezzi et al
\item Administrative details
\item pointInRegion(p)
\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{A Table for Assignment 4, Part 2, pointInRegion(p)}
\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 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 4}
\begin{itemize}
\item Limited guidance on test case selection
\item Improved test cases would have improved the results
\item Consider the method for deleting from a sequence of T (next slide)
\item We are moving toward automated testing
\item We have seen the advantages of regression testing
\item Some have adopted the excellent strategy of test as you develop
\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}
What test cases will highlight the error?
\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{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 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
\item Even implicit qualities should be verified
\begin{itemize}
\item Because requirements are often incomplete
\item For instance robustness, maintainability
\end{itemize}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment