Merge branch 'master' of https://gitlab.cas.mcmaster.ca/smiths/se2aa4_cs2me3

Assignments/A3/A3Soln/A3P1_Spec.tex

@@ -430,7 +430,7 @@ PathT($st, ornt, l$):
 \noindent len:
 \begin{itemize}
 \item output: \wss{Output the total number of points (grid cells) on the path,
-    including the beginning and end points (cells).}$out := +(l: \mbox{LineT} | i \in s: l.\mbox{len})$
+    including the beginning and end points (cells).}$out := +(l: \mbox{LineT} | l \in s: l.\mbox{len})$
 \item exception: None
 \end{itemize}
 

Lectures/L29_IntroductionToVerification/IntroductionToVerification.tex

@@ -481,35 +481,4 @@ Avoids potential ArrayIndexOutOfBoundsException Exception
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{frame}
-\frametitle{Does our Engineering Analogy Fail?}
-
-\begin{itemize}
-
-\item \structure{If a bridge can hold 512 kN, can it hold 499 kN?}
-\item \structure{If our software works for the input 512, will it work for 499?}
-
-\end{itemize}
-
-\end{frame}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\begin{frame}
-\frametitle{Verification in Engineering}
-
-\begin{itemize}
-
-\item Example of bridge design
-\item One test assures infinite correct situations
-\item In software a small change in the input may result in significantly different behaviour
-\item There are also chaotic systems in nature, but products of engineering
-  design are usually stable and well-behaved
-% consider the examples of weather, bifurcation in engineering, chaos theory for traffic, etc.
-\end{itemize}
-
-\end{frame}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
 \end{document}
\ No newline at end of file

Lectures/L30_IntroToVerificationContd/IntroToVerificationContd.tex

@@ -29,7 +29,7 @@
 \mode<presentation>{}
 
 \input{../def-beamer}
-\Drafttrue
+\Draftfalse
 
 \newcommand{\topicTitle}{30 Introduction to Verification Continued (Ch.\ 6)}
 \ifDraft
@@ -73,17 +73,20 @@ TBD
 {
 \begin{itemize}
 
-\item A3 deadlines
+\item A3
 \begin{itemize}
-\item Part 2 - Code: due 11:59 pm Mar 20
-\item {Part 1 spec available in repo}
+\item Part 2 - Code: due 11:59 pm Mar 26
 \end{itemize}
 
 \item A4
 \bi
-\item Now available in our repo
-\item Your own design and specification
-\item Due April 3 at 11:59 pm
+\item Due April 9 at 11:59 pm
+\item Might be tempted to write code first
+\bi
+\item Recommend starting with syntax of
+  module(s), state variables
+\item Maybe program a little before semantics part
+\ei
 \ei
 
 \end{itemize}
@@ -94,6 +97,35 @@ TBD
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\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, performance
+\end{itemize}
+\item \structure{What is better than implicitly specified
+    qualities?} % explicit!
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{frame}
 \frametitle{Approaches to Verification}
 
@@ -540,6 +572,15 @@ validity
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\begin{frame}
+\frametitle{Quality Testing: Installability}
+\begin{itemize}
+\item \structure{How might you test installability?} %virtual machines, docker
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{frame}
 \frametitle{Fault Testing}
 \begin{itemize}