diff --git a/Lectures/Figures/RevisedHierarchy.pdf b/Lectures/Figures/RevisedHierarchy.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..eba8842a17c61c11088e323d8259fe9f3048214b
Binary files /dev/null and b/Lectures/Figures/RevisedHierarchy.pdf differ
diff --git a/Lectures/L13_ModularDesign/ModularDesign.tex b/Lectures/L13_ModularDesign/ModularDesign.tex
index 4dd4a9e669bb33c7d356339e393500f329f677c4..e1fd5f8d038c1c1d6c6463d65de557002f2f5e04 100755
--- a/Lectures/L13_ModularDesign/ModularDesign.tex
+++ b/Lectures/L13_ModularDesign/ModularDesign.tex
@@ -70,7 +70,7 @@
 \item GitHub issues for colleagues
 \bi
 \item Assigned 1 colleague (see \texttt{Repos.xlsx} in repo)
-\item Provide at least 5 issues on their SRS
+\item Provide at least 5 issues on their VnV Plan
 \item Grading as before
 \item Due by Tuesday, Oct 30, 11:59 pm
 \ei
diff --git a/Lectures/L14_MIS/MIS.pdf b/Lectures/L14_MIS/MIS.pdf
index 28cf78829b45f08ead650f2637fdc61bd85df74d..d8c6e81db759cfed5d2279c7bd7b8e9dbab8fec3 100644
Binary files a/Lectures/L14_MIS/MIS.pdf and b/Lectures/L14_MIS/MIS.pdf differ
diff --git a/Lectures/L17_MathReview/MathReview.pdf b/Lectures/L17_MathReview/MathReview.pdf
index abef971625c025fb46bc75324ae5c539b7a37621..4f21eac04abe70bcb4dee11cb29e49a3e455743a 100644
Binary files a/Lectures/L17_MathReview/MathReview.pdf and b/Lectures/L17_MathReview/MathReview.pdf differ
diff --git a/Lectures/L17_MathReview/MathReview.tex b/Lectures/L17_MathReview/MathReview.tex
index ba9ac3b93b3e5c7e643a7908f76cf3c7203eca5e..dc16d062b335ea151763ae15cc863a51cbf33eda 100755
--- a/Lectures/L17_MathReview/MathReview.tex
+++ b/Lectures/L17_MathReview/MathReview.tex
@@ -16,6 +16,9 @@
     unicode=false}
 \urlstyle{same}
 
+\usepackage{booktabs}
+\usepackage{multirow}
+
 \bibliographystyle{plain}
 
 %\usetheme{Iimenau}
@@ -28,7 +31,7 @@
 
 \input{../def-beamer}
 
-\newcommand{\topic}{17 MIS Continued}
+\newcommand{\topic}{17 Math Review}
 
 \input{../titlepage}
 
@@ -39,12 +42,24 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-\frametitle{MIS Continued}
+\frametitle{Math Review}
 
 \bi
+\item MG Presentations
+\bi
+\item Steven
+\item Isobel
+\ei
 \item Administrative details
 \item Questions?
-\item License and copyright
+\item New Uses Relation for SWHS
+\item Math review introduction
+\item Review of sets, relations and functions
+\item Review of logic
+\item Review of types, sets, sequence and tuples
+\item Multiple assignment statement
+\item Conditional rules
+\item Finite state machines
 \ei
 \end{frame}
 
@@ -54,7 +69,15 @@
 \frametitle{Administrative Details}
 
 \bi
-\item admin points
+\item GitHub issues for colleagues
+\bi
+\item Assigned 1 colleague (see \texttt{Repos.xlsx} in repo)
+\item Provide at least 5 issues on their MG
+\item Grading as before
+\item Due by Tuesday, Nov 14, 11:59 pm
+\ei
+\item MG marking scheme in Avenue (soon)
+\item Updated MIS template in CAS 741 repo (soon)
 \ei
 
 \end{frame}
@@ -100,7 +123,531 @@ Final Documentation & Week 13 & Dec 6\\
 \begin{frame}
 \frametitle{Questions?}
 \begin{itemize}
-\item Questions about ...
+\item Questions about Module Guides?
+\item Questions about MIS?
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+
+\frametitle{Revised Uses Relation for SWHS}
+
+\begin{center}
+\includegraphics[scale=0.58]{../Figures/RevisedHierarchy.pdf}
+\end{center}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\begin{frame}
+\frametitle{Introduction}
+\begin{itemize}
+\item The material in these slides should hopefully be review, or
+  reasonably easy to pick up
+\item Shows the simple mathematics that can be used to build your MIS
+\item Shows a syntax that you can use
+\item The presentation follows \cite{HoffmanAndStrooper1995} (Chapter
+  3) and \cite{GriesAndSchneider1993}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Sets, Relations and Functions}
+\begin{itemize}
+\item A set is an unordered collection of elements
+\item A binary relation is a set of ordered pairs
+\item A function is a relation in which each element in the domain
+  appears exactly once as the first component in the ordered pair
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Sets}
+\begin{itemize}
+\item An element either belongs to a set or it does not
+\item $x \in S$ versus $x \notin S$
+\item Defining a set
+\begin{itemize}
+\item Enumerate $\{ x_1, x_2, x_3, ..., x_n \}$
+\item Logical condition (rule) $\{x | p(x) \}$
+\item Notation from \cite{GriesAndSchneider1993} $\{x: X | R : E \}$
+\item An integer range $[2 .. 4] = \{2, 3, 4\}$, $[7 .. 4] = \{\}$
+\end{itemize}
+\item Examples
+\begin{itemize}
+\item $S = \{ 1, 7, 6 \}$
+\item $S = \{ x |$ $x$ is an integer between $1$ and $4$ inclusive
+  $\}$
+\item $S = \{ x: \mathbb{N} |$ $0 \leq x \leq 4$ : $x$ $\}$
+%\item Clarify that there is no notion of ordering in sets
+\end{itemize}
+\item Does $\{ 1, 7, 6 \} = \{ 7, 1, 6 \}$?
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Relations}
+\begin{itemize}
+\item Let $<x, y>$ denote an ordered pair
+\begin{itemize}
+\item $dom(R) = \{x | <x, y> \in R\}$
+\item $ran(R) = \{y | <x, y> \in R\}$
+\end{itemize}
+\item Defining a relation
+\begin{itemize}
+\item Enumerate $\{ <0, 1>, <0, 2>, <2, 3> \}$
+\item Rule $\{ <x, y>|$ $x$ and $y$ are integers and $x < y \}$
+\item $\{ x, y: \mathbb{N} |$ $x < y$ : $<x, y> \}$
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Functions}
+\begin{itemize}
+\item Let $<x, y>$ denote an ordered pair
+\item Each element of the domain is associated with a unique element
+  of the range
+\item Defining a function
+\begin{itemize}
+\item Enumerate $\{ <0, 1>, <1, 2>, <2, 3> \}$
+\item Rule $\{ <x, y> |$ $x$ and $y$ are integers and $y = x^2 \}$
+\end{itemize}
+\item Notation
+\begin{itemize}
+\item $f(a) = b$ means $<a, b> \in f$
+\item $f(x) = x^2$
+\item $f: T_1 \rightarrow T_2$
+\item $\{ <<x_1, x_2>, y> |$ $x_1$, $x_2$ are integers and $y = x_1 + x_2 \}$
+\end{itemize}
+\item Is $\{ <0, 1>, <0, 2>, <2, 3> \}$ a function?
+\item Is $\{ <x, y> |$ $x$ and $y$ are integers and $y^2 = x\}$?
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Logic}
+\begin{itemize}
+\item A logical expression is a statement whose truth values can be
+  determined ($6 < 7$?)
+\item Truth values are either \emph{true} or \emph{false}
+\item Complex expressions are formed from simpler ones using logical
+  connectives ($\neg$, $\wedge$, $\vee$, $\rightarrow$,
+  $\leftrightarrow$)
+\item Truth tables
+\item Evaluation
+\begin{itemize}
+\item Decreasing order of precedence: $\neg$, $\wedge$, $\vee$,
+$\rightarrow$, $\leftrightarrow$
+\item Evaluate from left to right
+\item Use rules of boolean algebra
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Quantifiers}
+\begin{itemize}
+\item Variables are often used inside logical expressions
+\item Variables have types
+\item A type is a set of values from which the variable can take its value
+\item Often quantify a logical expression over a given variable
+\begin{itemize}
+\item Universal quantification
+\item Existential quantification
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Quantifiers Continued}
+
+\begin{itemize}
+\item Prefer \cite[p.\ 143]{GriesAndSchneider1993} notation for quantification
+  (and set building)
+\item $(*x: X | R : P)$ means application of the operator $*$ to the values $P$ for
+all $x$ of type $X$ for which range $R$ is true.  In the above equations, the
+$*$ operators include $\forall$, $\exists$ and $+$ are used
+\item Example on next slide for rank function specification
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+%\frametitle{Quantifiers Example for Rank Function}
+
+\noindent $\mbox{rank}(a, A): \mathbb{R} \times \mathbb{R}^n \rightarrow \mathbb{N}$\newline
+$\mbox{rank}(a, A) \equiv \mbox{avg}(\mbox{indexSet}(a, \mbox{sort}(A)))$\newline
+
+\noindent $\mbox{indexSet}(a, B): \mathbb{R} \times \mathbb{R}^n \rightarrow \mbox{ set of }
+\mathbb{N}$\newline
+$\mbox{indexSet}(a, B) \equiv \{j: \mathbb{N} | j \in [1..|B|]
+\wedge B_j = a : j \}$\newline
+
+\noindent $\mbox{sort}(A): \mathbb{R}^n \rightarrow \mathbb{R}^n$\newline
+$\mbox{sort}(A) \equiv B: \mathbb{R}^n, \mbox{ such that }$\newline
+$\forall (a: \mathbb{R} | a \in A : \exists(b: \mathbb{R} | b \in B: b = a)
+\wedge \mbox{count}(a, A) = \mbox{count}(b, B)) \wedge \forall (i: \mathbb{N} | i \in [1..|A|-1] : B_i \leq B_{i+1})$\newline
+
+\noindent $\mbox{count}(a, A): \mathbb{R} \times \mathbb{R}^n \rightarrow \mathbb{N}$\newline
+$\mbox{count}(a, A): + (x: \mathbb{N} | x \in A \wedge x = a : 1)$\newline
+
+\noindent $\mbox{avg}(C): \mbox{ set of } \mathbb{N} \rightarrow \mathbb{R}$\newline
+$\mbox{avg}(C) \equiv + (x: \mathbb{N} | x \in C : x) / |C|$\newline
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Quantifiers Continued}
+\begin{itemize}
+\item Bound variables appear in the scope of the quantifier
+\item Free variables are not bound to any quantifier
+\item Free variables in an expression often  mean that we cannot determine the truth value of the expression
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Types, Sets, Sequence and Tuples}
+\begin{itemize}
+\item A type is a set of values, so any precisely defined set is a type
+\item Primitive types are often integer, boolean, character, string
+  and real
+\item Types can include functions ($T_1 \rightarrow T_2$)
+\item User-defined types
+\begin{itemize}
+\item The set of values has to be given
+\item Often use type constructors
+\end{itemize}
+\item Useful type constructors
+\begin{itemize}
+\item Set
+\item Sequence
+\item Tuple
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Types}
+\begin{itemize}
+\item Specify the type of a variable
+\begin{itemize}
+\item $x_1, x_2, ..., x_n : T$
+\item $x: integer$
+\item $a, b, c: string$
+\end{itemize}
+\item Type definition
+\begin{itemize}
+\item $T = d$
+\item $float = real$
+\item $colour = \{red, white, blue \}$
+\item $testtype = \{uniaxial, biaxial, shear \}$
+\item $x: testtype$
+\item $motionT = \{ forward, backward, stop \}$
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Primitive Types}
+\begin{itemize}
+\item Integer
+\begin{itemize}
+\item $\{ ... -2, -1, 0, 1, 2, ... \}$
+\item $+, -, \times, /$
+\item $=, \neq$
+\item $<, \leq, \geq, >$
+\end{itemize}
+\item Real
+\begin{itemize}
+\item $\{ all~real~numbers \}$
+\item $+, -, \times, /, \sin (), \cos (), \exp ()$ etc.
+\item $=, \neq$
+\item $<, \leq, \geq, >$
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Primitive Types Continued}
+\begin{itemize}
+\item Boolean type
+\begin{itemize}
+\item $\{ true, false \}$
+\item $\neg$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$
+\end{itemize}
+\item Char type
+\begin{itemize}
+\item Set of ASCII characters
+\item Character values appear in quotes $'a'$, $'b'$, $'c'$, etc.
+\item $=, \neq$
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Primitive Types Continued}
+\begin{itemize}
+\item String type
+\begin{itemize}
+\item All finite sequences of characters
+\item String constants are in double quotes $''abc''$
+\item $s[i..j]$ is the substring of $s$ from position $i$ to position $j$
+\item $s_1 || s_2$ concatenates strings $s_1$ and $s_2$
+\item $=, \neq$ for is equal and not equal
+\item $\in, \notin$ for is member and not a member
+\item $s[i]$ is the $i$th character of $s$
+\item $|s|$ is the length of $s$
+\item Positions in strings are zero relative
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Sets}
+\begin{itemize}
+\item A set is an unordered collection of elements of the same type
+\item Declare a set of type $T$ as $set~of~T$
+\item Example
+\begin{itemize}
+\item $T = set~of~ \{red, green, blue \}$ defines type $T$ as the power set of $\{red, green, blue \}$
+\item $x: set~of~integer$
+\end{itemize}
+\item What are some possible values for $x: set~of~integer$?
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Operations on Sets}
+\begin{itemize}
+\item $\cup$ union
+\item $\cap$ intersection
+\item $-$ difference
+\item $\times$ Cartesian product
+\item $=, \neq$ equal, not equal
+\item $\in, \notin$ member, non-member
+\item $|s|$ size of set $s$
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Sequences}
+\begin{itemize}
+\item A sequence is an ordered collection of elements of the same type
+\begin{itemize}
+\item Elements can occur more than once
+\item Sometimes referred to as a list
+\item Similar to an array
+\end{itemize}
+\item Declare a sequence of type $T$ by $sequence~of~T$
+\item $< x_0, x_1, ..., x_n >$ for $n \geq 0$ for a sequence with elements $x_0, x_1, ..., x_n$
+\item $< >$ is the empty sequence
+\item Position in a sequence is zero relative
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Sequences Continued}
+\begin{itemize}
+\item Examples
+\begin{itemize}
+\item $T = sequence~of~\{ red, green, blue \}$ defines the type $T$ as the set of all sequences of elements from
+$\{red, green, blue \}$
+\item $x: sequence~of~integer$
+\end{itemize}
+\item Fixed-length sequence of type $T$ with length $l$
+\begin{itemize}
+\item $sequence~[l]~of~T$
+\item $l$ is a positive integer
+\item $sequence~[l_1, l_2, ..., l_n ]~of~T$ is a shorthand for $sequence~[l_1]~of~sequence~[l_2]~of ... sequence~
+[l_n]~ of~T$
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Operations on Sequences}
+\begin{itemize}
+\item $s[i..j]$ is the subsequence of $s$ from position $i$ to position $j$
+\item $s[i..j]$ is undefined if $i \notin [0..|s|-1] \vee j \notin [0 .. |s|-1]$
+\item $s_1 || s_2$ concatenates sequences $s_1$ and $s_2$
+\item $=, \neq$ for is equal and not equal
+\item $\in, \notin$ for is member and not a member
+\item $s[i]$ is the $i$th element of $s$
+\item $s[i]$ is undefined if $i \notin [0..|s|-1]$
+\item $|s|$ is the length of $s$
+\item A string is a sequence of characters
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Tuples}
+\begin{itemize}
+\item A tuple is a collection of elements of possibly different types
+\item Each tuple has one or more fields
+\item Each field has a unique identifier called the field name
+\item Similar to a record or a structure
+\item To declare a tuple use
+\begin{itemize}
+\item $tuple~of~(f_1: T_1, f_2: T_2, ..., f_n: T_n )$ with $n \geq 1$
+\item $f_i$ is the name of the $i$th field
+\item $T_i$ is the type of the $i$th field
+\item $tuple~of~(f_1, f_2, ..., f_n: T )$ if all fields are of the same type
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Example Tuples}
+\begin{itemize}
+\item Examples
+\begin{itemize}
+\item $pair = tuple~of~(id: integer, val: string)$
+\item $experimentT = tuple~of~(b_{cond}: bcondT, control: controlT)$
+\end{itemize}
+\item Define the value of a tuple by using an expression of the form
+\begin{itemize}
+\item $<x_1, x_2, ..., x_n >$
+\item $<4, ''cat''>$ is a value of type pair
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Operations on Tuples}
+\begin{itemize}
+\item $=, \neq$ equal, not equal
+\item $t.f$ is the value of field $f$ of tuple $t$
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Using Type Constructors}
+\begin{itemize}
+\item $bcondT = \{ uniaxial, biaxial, multiaxial, shear \}$
+\item $controlT = \{ load\_controlled, displacement\_controlled \}$
+\item $experimentT = tuple~of~(b_{cond}: bcondT, control: controlT)$
+\item $experiment: experimentT$
+\item $directionT = \{clockwise, counterclockwise \}$
+\item $powerT = [MIN\_POWER ... MAX\_POWER]$
+\item $motorT = tuple~of~ (powerOn: Boolean,~direction: directionT,~powerLevel: powerT)$
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Multiple Assignment Statement}
+\begin{itemize}
+\item $v_1, v_2, ..., v_n := e_1, e_2, ...,, e_n$ with $n \geq 1$
+\item The $v_i$s are distinct variables and each $e_i$ is an expression of the same type as $v_i$
+\item Compute the values of all the expression $e_i$ and then assign these values simultaneously
+\item Example
+\begin{itemize}
+\item $x, y := 0, 10$
+\item $x, y := 10, x$
+\item $x, y := y, x$
+\end{itemize}
+\item Convenient for defining the meaning of pieces of code
+\item Use as a function on the state space of a program
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Conditional Rules}
+\begin{itemize}
+\item $(c_1 \Rightarrow r_1 | ... | c_n \Rightarrow r_n )$, where $n \geq 1$
+\item $c_i$s are the logical expressions
+\item $r_i$s are the rules
+\item $c_i \Rightarrow r_i$ is the $i$th component of the rule
+\item The first $c_i$ that evaluates to true applies rule $r_i$
+\item If no condition is true then the conditional rule is undefined
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Uses of Conditional Rules}
+\begin{itemize}
+\item To define the value of a function
+\item $min(x,y) = (x \leq y \Rightarrow x | x > y \Rightarrow y)$
+\item To define the meaning of a program
+\begin{itemize}
+\item If $(x < y)$ then $z := x$ else $z := y$
+\item $(x < y \Rightarrow z := x | x \geq y \Rightarrow z:= y)$
+\item $(x < y \Rightarrow x, y := x, y | x \geq y \Rightarrow x, y := y, x)$
+\end{itemize}
+\item Conditional rules can be expressed in tables
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Finite State Machines}
+\begin{itemize}
+\item A FSM is a tuple $(S, s_0, I, O_E, O_O, T, E, C)$ where
+\item $S$ is a finite set of states
+\item $s_0$ is the initial state in $S$ $(s_0 \in S)$
+\item $I$ is a finite set of inputs
+\item $T: S \times I \rightarrow S$ is the transition function
+\item $O_E$ is a finite set of event outputs
+\item $E: S\times I \rightarrow O_E$ is the event output
+\item $O_C$ is a finite set of condition outputs
+\item $C: S \rightarrow O_C$ is the condition output
 \end{itemize}
 \end{frame}
 
diff --git a/Lectures/L18_MISContinued/MISContinued.pdf b/Lectures/L18_MISContinued/MISContinued.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..77c33536d75e380dc1f5e06290294f7c7c2dcbde
Binary files /dev/null and b/Lectures/L18_MISContinued/MISContinued.pdf differ
diff --git a/Lectures/L18_MISContinued/MISContinued.tex b/Lectures/L18_MISContinued/MISContinued.tex
new file mode 100755
index 0000000000000000000000000000000000000000..41f4e33155c6dc52b129f5aacc2a3efb11f1002e
--- /dev/null
+++ b/Lectures/L18_MISContinued/MISContinued.tex
@@ -0,0 +1,924 @@
+%\documentclass[handout]{beamer} 
+\documentclass[t,12pt,numbers,fleqn]{beamer}
+%\documentclass[ignorenonframetext]{beamer}
+
+\newif\ifquestions
+%\questionstrue
+\questionsfalse
+
+\usepackage{pgfpages} 
+\usepackage{hyperref}
+\hypersetup{colorlinks=true,
+    linkcolor=blue,
+    citecolor=blue,
+    filecolor=blue,
+    urlcolor=blue,
+    unicode=false}
+\urlstyle{same}
+
+\usepackage{booktabs}
+\usepackage{multirow}
+
+\bibliographystyle{plain}
+
+%\usetheme{Iimenau}
+
+\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}{18 MIS Continued}
+
+\input{../titlepage}
+
+\begin{document}
+
+\input{../footline}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{MIS Continued}
+
+\bi
+\item Administrative details
+\item Questions?
+\ei
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Administrative Details}
+
+\bi
+\item admin points
+\ei
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Administrative Details: Deadlines}
+~\newline
+\begin{tabular}{l l l}
+\textbf{MG} & Week 09 & Nov 8\\
+\textbf{MIS Present} & Week 10 & Week of Nov 13\\
+\textbf{MIS} & Week 11 & Nov 22\\
+Impl.\ Present & Week 12 & Week of Nov 27\\
+Final Documentation & Week 13 & Dec 6\\
+\end {tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Administrative Details: Presentation Schedule}
+
+\bi
+\item MIS Present
+\bi
+\item \textbf{Tuesday: Isobel, Keshav, Paul}
+\item \textbf{Friday: Shusheng, Xiaoye, Devi}
+\ei
+\item Impl.\ Present
+\bi
+\item Tuesday: Alexander S., Steven, Alexandre P.
+\item Friday: Jason, Geneva, Yuzhi
+\ei
+
+\ei
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Questions?}
+\begin{itemize}
+\item Questions about ...
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+
+\frametitle{Exception Signaling}
+
+\begin{itemize}
+\item Useful to think about exceptions in the design process
+\item Will need to decide how exception signalling will be done
+\begin{itemize}
+\item A special return value, a special status parameter, a global variable
+\item Invoking an exception procedure
+\item Using built-in language constructs
+\end{itemize}
+\item Caused by errors made by programmers, not by users
+\item Write code so that it avoid exceptions
+\item Exceptions will be particularly useful during testing
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+
+\frametitle{Assumptions versus Exceptions}
+
+\begin{itemize}
+\item The assumptions section lists assumptions the module developer is permitted to make about the programmer's behaviour
+\item Assumptions are expressed in prose
+\item Use assumptions to simplify the MIS and to reduce the complexity of the final implementation
+\item Interface design should provide the programmer with a means to check so that they can avoid exceptions
+\item When an exceptions occurs no state transitions should take place, any output is {\it don't care}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+
+\frametitle{Quality Criteria}
+
+\begin{itemize}
+\item Consistent
+\begin{itemize}
+\item Name conventions
+\item Ordering of parameters in argument lists
+\item Exception handling, etc.
+\end{itemize}
+\item Essential - omit unnecessary features
+\item General - cannot always predict how the module will be used
+\item As implementation independent as possible
+\item Minimal - avoid access routines with two potentially independent services
+\item High cohesion - components are closely related
+\item Low coupling - not strongly dependent on other modules
+\item Opaque - information hiding
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+
+\frametitle{SWHS Example}
+
+Look at SWHS repo
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Modules with External Interaction}
+
+\begin{itemize}
+\item In general, some modules may interact with the environment or other modules
+%\item The Display Point Masses Applet module does this
+\item Environment might include the keyboard, the screen, the file system, motors, sensors, etc.
+\item Sometimes the interaction is informally specified using prose (natural language)
+\item Can introduce an environment variable
+\begin{itemize}
+\item Name, type
+\item Interpretation
+\end{itemize}
+\item Environment variables include the screen, the state of a motor (on, direction of rotation, power level, etc.),
+the position of a robot
+
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{External Interaction Continued}
+
+\begin{itemize}
+\item Some external interactions are hidden
+\begin{itemize}
+\item Present in the implementation, but not in the MIS
+\item An example might be OS memory allocation calls
+\end{itemize}
+\item External interaction described in the MIS
+\begin{itemize}
+\item Naming access programs of the other modules
+\item Specifying how the other module's state variables are changed
+\item The MIS should identify what external modules are used
+\end{itemize}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{MIS for GUI Modules}
+
+\begin{itemize}
+\item Could introduce an environment variable
+\item window: sequence [RES\_H][RES\_V] of pixelT
+\begin{itemize}
+\item Where window[r][c] is the pixel located at row r and column c, with numbering zero-relative and beginning at the
+upper left corner
+\item Would still need to define pixelT
+\end{itemize}
+\item Could formally specify the environment variable transitions
+\item More often it is reasonable to specify the transition in prose
+\item In some cases the proposed GUI might be shown by rough sketches
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Display Point Masses Module Syntax}
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exc}\\
+\hline
+DisplayPointMassesApplet & ~ & DisplayPointMassesApplet & ~\\
+\hline
+paint & ~ & ~ & ~\\
+\hline
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Display Point Masses Module Semantics}
+
+\textbf{Environment Variables}\\
+$\mathit{win}:$ 2D sequence of pixels displayed within a web-browser \\
+
+\noindent DisplayPointMassesApplet():
+\begin{itemize}
+\item transition: The state of the abstract object ListPointMasses is modified as follows:\\
+ListPointMasses.init()\\
+ListPointMasses.add(0, PointMassT(20, 20, 10))\\
+ListPointMasses.add(1, PointMassT(120, 200, 20))\\
+...
+\end{itemize}
+
+\noindent paint():
+\begin{itemize}
+\item transition $win := $ Modify window so that the point masses in ListPointMasses 
+are plotted as circles.  The centre of each circles should be the corresponding x and y coordinates and the radius should
+be the mass of the point mass.
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Specification of ADTs}
+\begin{itemize}
+\item Similar template to abstract objects
+\item ``Template Module'' as opposed to ``Module''
+\item ``Exported Types'' that are abstract use a ?
+\begin{itemize}
+\item pointT = ?
+\item pointMassT = ?
+\end{itemize}
+\item Access routines know which abstract object called them
+\item Use ``self'' to refer to the current abstract object
+\item Use a dot ``.'' to reference methods of an abstract object
+\begin{itemize}
+\item $p.\mbox{xcoord()}$
+\item $\mathit{self}.pt.\mbox{dist}(p.\mbox{point}())$
+\end{itemize}
+\item Similar notation to Java
+\item The syntax of the interface in C is different
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Syntax Line ADT Module}
+
+\textbf{Template Module}\\
+~\newline
+lineADT\\
+~\newline
+\textbf{Uses}\\
+~\newline
+pointADT\\
+~\newline
+\textbf{Exported Types}\\
+~\newline
+lineT = ?
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Syntax Line ADT Module Continued}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+new lineT & pointT, pointT & lineT & ~\\
+\hline
+start & ~ & pointT & ~\\
+\hline
+end & ~ & pointT & ~\\
+\hline 
+length & ~ & real & ~\\
+\hline
+midpoint & ~ & pointT & ~\\
+\hline
+rotate & real & ~ & ~\\
+\hline
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Semantics Line ADT Module}
+
+\textbf{State Variables}\\
+~\newline
+$s$: pointT\\
+$e$: pointT\\
+~\newline
+\textbf {State Invariant}\\
+~\newline
+None\\
+~\newline
+\textbf{Assumptions}\\
+~\newline
+None
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics Line ADT Module}
+
+\noindent new lineT ($p_1, p_2$):
+\begin{itemize}
+\item transition: $s, e := p_1, p_2$
+\item output: $out := \mathit{self}$
+\item exception: none
+\end{itemize}
+
+\noindent start:
+\begin{itemize}
+\item output: $out := s$
+\item exception: none
+\end{itemize}
+
+\noindent end:
+\begin{itemize}
+\item output: $out := e$
+\item exception: none
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics Continued}
+
+\noindent length:
+\begin{itemize}
+\item output: $out := s.\mathrm{dist}(e)$
+\item exception: none
+\end{itemize}
+
+\noindent midpoint:
+\begin{itemize}
+\item output: $out := $
+$$\mathrm{new~} \mathrm{pointT} (\mathrm{avg}(s.\mathrm{xcoord}, e.\mathrm{xcoord}), \mathrm{avg}(s.\mathrm{ycoord},
+e.\mathrm{ycoord}))$$
+\item exception: none
+\end{itemize}
+
+\noindent rotate ($\phi$):\\
+$\phi$ is in radians
+\begin{itemize}
+\item transition: $s.\mathrm{rotate}(\phi), e.\mathrm{rotate}(\phi)$
+\item exception: none
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Line ADT Local Functions}
+
+\textbf{Local Functions}\\
+~\newline
+avg: real $\times$ real $\rightarrow$ real
+
+\noindent avg($x_1, x_2$) $\equiv \frac{x_1 + x_2}{2}$
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% \begin{frame}
+% \frametitle{ADTs in C}
+
+% \begin{itemize}
+% \item Each object will be a pointer to a struct that holds its state
+% \item The interface for each routine, other than initialization routines, will need this pointer
+% \item There is an implicit object of the ADT type as the first input parameter in all routines other than init
+% \item Need to add a prefix to all routines, other than initialization routines, to avoid naming conflicts
+% \item For PointADT, using prefix {\tt pt\_}
+% \begin{itemize}
+% \item {\tt typedef struct Point* pointT;}
+% \item \uncover<2->{\tt pointT pt\_init(float x, float y);}
+% \item \uncover<3->{\tt float pt\_xcoord(pointT self);}
+% \item \uncover<4->{\tt float pt\_ycoord(pointT self);}
+% \item \uncover<5->{\tt float pt\_dist(pointT self, pointT p);}
+% \end{itemize}
+% \item For PointMassADT use prefix {\tt pm\_}
+% \end{itemize}
+% \end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Generic Modules}
+
+\begin{itemize}
+\item What if we have a sequence of integers, instead of a sequence of point masses?
+\item What if we want a stack of integers, or characters, or pointT, or pointMassT?
+\item Do we need a new specification for each new abstract object?
+\item No, we can have a single abstract specification implementing a family of abstract objects that are distinguished
+only by a few variabilities
+\item Rather than duplicate nearly identical modules, we parameterize one \structure{generic module} with respect to
+type(s)
+\item Advantages
+\begin{itemize}
+\item Eliminate chance of inconsistencies between modules
+\item Localize effects of possible modifications
+\item Reuse
+\end{itemize}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Generic Stack Module Syntax}
+
+\textbf{Generic Module}\\
+~\newline
+Stack(T)\\
+~\newline
+\textbf{Exported Constants}\\
+~\newline
+$\mbox{MAX\_SIZE} = 100$
+~\newline
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+... & ... & ... & ...\\
+\hline
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Stack Module Syntax}
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+s\_init & ~ & ~ & ~\\
+\hline
+s\_push & T & ~ & FULL\\
+\hline
+s\_pop & ~ & ~ & EMPTY\\
+\hline
+s\_top & ~ & T & EMPTY\\
+\hline
+s\_depth & ~ & integer & ~\\
+\hline
+\end{tabular}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Semantics}
+
+\textbf{State Variables}\\
+~\newline
+\uncover<2->{\structure<2>{$s$: sequence of T}}\\
+~\newline
+\textbf{State Invariant}\\
+~\newline
+\uncover<3->{\structure<3>{$|s| \leq \mbox{MAX\_SIZE}$}}\\
+~\newline
+\textbf{Assumptions}\\
+~\newline
+\uncover<4->{\structure<4>{s\_init() is called before any other access routine}}\\
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics}
+
+s\_init():
+\begin{itemize}
+\item transition: \uncover<2->{\structure<2>{$s := <>$}}
+\item exception: \uncover<3->{\structure<3>{none}}
+\end{itemize}
+
+\noindent s\_push(x):
+\begin{itemize}
+\item transition: \uncover<4->{\structure<4>{$s := s || <x>$}}
+\item exception: \uncover<5->{\structure<5>{$exc := (|s| = \mbox{MAX\_SIZE} \Rightarrow \mbox{FULL})$}}
+\end{itemize}
+
+\noindent s\_pop():
+\begin{itemize}
+\item transition: \uncover<6->{\structure<6>{$s := s[0..|s| - 2]$}}
+\item exception: \uncover<7->{\structure<7>{$exc := (|s| = 0 \Rightarrow \mbox{EMPTY})$}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Access Routine Semantics Continued}
+
+\noindent s\_top():
+\begin{itemize}
+\item output: \uncover<2->{\structure<2>{$out := s[|s| - 1]$}}
+\item exception: \uncover<3->{\structure<3>{$exc := (|s| = 0 \Rightarrow \mbox{EMPTY})$}}
+\end{itemize}
+
+\noindent s\_depth():
+\begin{itemize}
+\item output: \uncover<4->{\structure<4>{$out := |s|$}}
+\item exception: \uncover<5->{\structure<5>{none}}
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Stack Module Properties}
+
+$\{ \mathit{true} \}$
+
+~~~~~s\_init()
+
+$\{ | s' | = 0 \}$
+
+~\newline
+$\{ | s | < \mbox{MAX\_SIZE} \}$
+
+~~~~~s\_push($x$)
+
+$\{ | s' | = | s | + 1 \wedge s'[|s'| - 1] = x \wedge s'[0..|s|-1] = s[0..|s|-1] \}$
+
+~\newline
+$\{ |s| < \mbox{MAX\_SIZE} \}$
+
+~~~~~s\_push($x$)\\
+~~~~~s\_pop()
+
+$s' = s$
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Object Oriented Design}
+\begin{itemize}
+\item One kind of module, ADT, called class
+\item A class exports operations (procedures) to manipulate instance objects (often called methods)
+\item Instance objects accessible via references
+\item Can have multiple instances of the class (class can be thought of as roughly corresponding to the notion of a type)
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Inheritance}
+\begin{itemize}
+\item Another relation between modules (in addition to USES and IS\_COMPONENT\_OF)
+\item ADTs may be organized in a hierarchy
+\item Class B may specialize class A
+\begin{itemize}
+\item B inherits from A
+\item Conversely, A generalizes B
+\end{itemize}
+\item A is a superclass of B
+\item B is a subclass of A
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Template Module Employee}
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Except}\\
+\hline
+Employee & string, string, moneyT & Employee & ~\\
+\hline
+first\_Name & ~ & string & ~\\
+\hline
+last\_Name & ~ & string & ~\\
+\hline
+where & ~ & siteT & ~\\
+\hline
+salary & ~ & moneyT & ~\\
+\hline
+fire & ~ & ~ & ~\\
+\hline
+assign & siteT & ~ & ~\\
+\hline
+\end{tabular}\\
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Inheritance Examples}
+
+\textbf{Template Module}
+Administrative\_Staff \textbf{inherits} Employee\\
+~\newline
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exception}\\
+\hline
+do\_this & folderT & ~ & ~\\
+\hline
+\end{tabular}\\
+~\newline
+
+\textbf{Template Module}
+Technical\_Staff \textbf{inherits} Employee\\
+~\newline
+
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exception}\\
+\hline
+get\_skill & ~ & skillT & ~\\
+\hline
+def\_skill & skillT & ~ & ~\\
+\hline
+\end{tabular}\\
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Inheritance Continued}
+
+\begin{itemize}
+\item A way of building software incrementally
+\item Useful for long lived applications because new features can be added without breaking the old applications
+\item A subclass defines a subtype
+\item A subtype is substitutable for the parent type
+\item Polymorphism - a variable referring to type A can refer to an object of type B if B is a subclass of A
+\item Dynamic binding - the method invoked through a reference depends on the type of the object associated with the
+reference at runtime
+\item All instances of the sub-class are instances of the super-class, so the type of the sub-class is a subtype
+\item All instances of Administrative\_Staff and Technical\_Staff are instances of Employee
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% \begin{frame}
+% \frametitle{Inheritance Continued}
+
+% emp1, emp2: Employee\\
+% emp3: Technical\_Staff\\
+
+% emp1 = Administrative\_Staff() \uncover<2->{\structure{$\surd$}}\\
+% emp2 = Technical\_Staff() \uncover<3->{\structure{$\surd$}}\\
+% emp3 = emp1 \uncover<4->{\structure{$\times$}}\\
+% emp3 = (Technical\_Staff) emp1 \uncover<5->{\structure{$\surd$}}\\
+% ~\newline
+% \uncover<6->{Polymorphism: type of RHS must be a subtype of the LHS}
+% \end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Dynamic Binding}
+
+\begin{itemize}
+\item Many languages, like C, use static type checking
+\item OO languages use dynamic type checking as the default
+\item There is a difference between a \structure{type} and a \structure{class} once we know this
+\begin{itemize}
+\item Types are known at compile time
+\item The class of an object may be known only at run time
+\end{itemize}
+\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Point ADT Module}
+
+\textbf{Template Module}\\
+~\newline
+PointT\\
+~\newline
+\textbf{Uses}\\
+~\newline
+N/A\\
+~\newline
+\textbf{Syntax}\\
+~\newline
+\textbf{Exported Types}\\
+~\newline
+PointT = ?\\
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Point ADT Module Continued}
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+new PointT & real, real & PointT & ~\\
+\hline
+xcoord & ~ & real & ~\\
+\hline
+ycoord & ~ & real & ~\\
+\hline
+dist & PointT & real & ~\\
+\hline
+\end{tabular}
+
+~\newline
+\textbf{Semantics}\\
+~\newline
+\textbf{State Variables}\\
+~\newline
+$xc$: real\\
+$yc$: real
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Point Mass ADT Module}
+
+\textbf{Template Module}\\
+~\newline
+PointMassT \textbf{inherits} PointT\\
+~\newline
+\textbf{Uses}\\
+~\newline
+PointT\\
+~\newline
+\textbf{Syntax}\\
+~\newline
+\textbf{Exported Types}\\
+~\newline
+PointMassT = ?\\
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Point Mass ADT Module Continued}
+
+\textbf{Exported Access Programs}\\
+~\newline
+\begin{tabular}{| l | l | l | l |}
+\hline
+\textbf{Routine name} & \textbf{In} & \textbf{Out} & \textbf{Exceptions}\\
+\hline
+new PointMassT & real, real, real & PointMassT & NegMassExcep\\
+\hline
+mval & ~ & real & ~\\
+\hline 
+force & PointMassT & real & ~\\
+\hline
+fx & PointMassT & real & ~\\
+\hline
+\end{tabular}
+
+~\newline
+\textbf{Semantics}\\
+~\newline
+\textbf{State Variables}\\
+~\newline
+$ms$: real
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Point Mass ADT Module Semantics}
+
+\noindent new PointMassT($x, y, m$):
+\begin{itemize}
+\item transition: $xc, yc, ms := x, y, m$
+\item output: $out := \mathit{self}$
+\item exception: $exc := (m < 0 \Rightarrow \mbox{NegativeMassException})$
+\end{itemize}
+~\newline
+\noindent force($p$):
+\begin{itemize}
+\item output: $$out := \mathrm{UNIVERAL\_G} \frac{\mathit{self}.ms \times p.ms}
+{\mathit{self}.\mathrm{dist}(p)^2}$$
+\item exception: none
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+\frametitle{Examples}
+
+\begin{itemize}
+\item Example Point Line and Circle
+\item Example Robot Path
+\item Example Vector Space
+\item Example Othello Program
+\item Example Maze Formal Specification (Dr.\ v.\ Mohrenschildt)
+\item Mustafa ElSheikh Mesh Generator \cite{CaretteEtAl2011}
+\item Wen Yu Mesh Generator \cite{SmithAndYu2009}
+\item Sven Barendt Filtered Backprojection
+\item Sanchez sDFT
+\end{itemize}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}[allowframebreaks]
+\frametitle{References}
+
+\bibliography{../../ReferenceMaterial/References}
+
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
\ No newline at end of file
diff --git a/Lectures/L21_CodeGen/CodeGen.tex b/Lectures/L21_CodeGen/CodeGen.tex
index e6ee27ebecb47b48bfcea3a13319a043e447e503..cfe03f8db9c886d5862662772c4ddacaa457c825 100755
--- a/Lectures/L21_CodeGen/CodeGen.tex
+++ b/Lectures/L21_CodeGen/CodeGen.tex
@@ -44,6 +44,7 @@
 \bi
 \item Administrative details
 \item Questions?
+\item License and copyright
 \ei
 \end{frame}
 
diff --git a/ReferenceMaterial/References.bib b/ReferenceMaterial/References.bib
index 43c0a5895e114ca8e07270391bf40fa6550129ae..a7bb2efafd15bde8d5c5b68db5f32fe5e2d31e9a 100644
--- a/ReferenceMaterial/References.bib
+++ b/ReferenceMaterial/References.bib
@@ -2,13 +2,23 @@
 %% http://bibdesk.sourceforge.net/
 
 
-%% Created for Spencer Smith at 2017-10-26 23:38:10 -0400 
+%% Created for Spencer Smith at 2017-11-06 10:09:39 -0500 
 
 
 %% Saved with string encoding Unicode (UTF-8) 
 
 
 
+@book{GriesAndSchneider1993,
+	Address = {New York},
+	Author = {David Gries and Fred B. Schneider},
+	Date-Added = {2017-11-06 15:09:37 +0000},
+	Date-Modified = {2017-11-06 15:09:37 +0000},
+	Keywords = {discrete mathematics},
+	Publisher = {Springer-Verlag Inc.},
+	Title = {A logical approach to discrete math},
+	Year = {1993}}
+
 @inproceedings{CaretteEtAl2011,
 	Abstract = {We present the design and implementation of a generative geometric kernel. The kernel generator is generic, type-safe, parametrized by many design-level choices and extensible.  The resulting code has minimal traces of the design abstractions.  We achieve genericity through a layered design deriving concepts from affine geometry, linear algebra and abstract algebra.  We achieve parametrization and type-safety by using OCaml's module system, including higher order modules. The cost of abstraction is removed by using MetaOCaml's support for code generation coupled with some annotations atop the code type.},
 	Author = {Jacques Carette and Mustafa ElSheikh and W. Spencer Smith},