Index: doc/theses/mike_brooks_MMath/array.tex
===================================================================
--- doc/theses/mike_brooks_MMath/array.tex	(revision d3942b9eeb219288b12ece12702144a21189a2b4)
+++ doc/theses/mike_brooks_MMath/array.tex	(revision 42d81a7e47cbd21d6203945bd49cc404cd002be2)
@@ -502,5 +502,82 @@
 \end{itemize}
 
-TODO: summarize the C rules and add the case-comparison table
+The traditional C rules are:
+\begin{itemize}
+\item
+	Reject a Statically Evaluable pair, if the expressions have two different values.
+\item
+	Otherwise, accept.
+\end{itemize}
+
+
+\newcommand{\falsealarm}{{\color{orange}\small{*}}}
+\newcommand{\allowmisuse}{{\color{red}\textbf{!}}}
+\newcommand{\cmark}{\ding{51}} % from pifont
+\newcommand{\xmark}{\ding{55}}
+\begin{figure}
+	\begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
+	 & \multicolumn{2}{c}{\underline{Values Equal}}
+	 & \multicolumn{2}{c}{\underline{Values Unequal}} 
+	 & \\
+	\textbf{Case}                                & C      & \CFA                & C                      & \CFA    & Compat. \\
+	Both Statically Evaluable, Same Symbol       & Accept & Accept              &                        &         & \cmark \\
+	Both Statically Evaluable, Different Symbols & Accept & Accept              & Reject                 & Reject  & \cmark \\
+	Both Dynamic but Stable, Same Symbol         & Accept & Accept              &                        &         & \cmark \\
+	Both Dynamic but Stable, Different Symbols   & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
+	Both Potentially Unstable, Same Symbol       & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
+	Any other grouping, Different Symbol         & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark
+	\end{tabular}
+
+	\vspace{12pt}
+	\noindent\textbf{Legend:}
+	\begin{itemize}
+	\item
+		Each row gives the treatment of a test harness of the form
+		\begin{cfa}
+			float x[ expr1 ];
+			float (*xp)[ expr2 ] = &x;
+		\end{cfa}
+		where \lstinline{expr1} and \lstinline{expr2} are metavariables varying according to the row's Case.
+		Each row's claim applies to other harnesses too, including,
+		\begin{itemize}
+		\item
+			calling a function with a paramter like \lstinline{x} and an argument of the \lstinline{xp} type,
+		\item
+			assignment in place of initialization,
+		\item
+			using references in place of pointers, and
+		\item
+			for the \CFA array, calling a polymorphic function on two \lstinline{T}-typed parameters with \lstinline{&x}- and \lstinline{xp}-typed arguments.
+		\end{itemize}
+	\item
+		Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
+		even though most test harnesses are asymetric.
+	\item
+		The table treats symbolic identity (Same/Different on rows)
+		apart from value eqality (Equal/Unequal on columns).
+		\begin{itemize}
+		\item
+			The expressions \lstinline{1}, \lstinline{0+1} and \lstinline{n}
+			(where \lstinline{n} is a variable with value 1),
+			are all different symbols with the value 1.
+		\item
+			The column distinction expresses ground truth about whether an omniscient analysis should accept or reject.
+		\item
+			The row distinction expresses the simple static factors used by today's analyses.
+		\end{itemize}
+	\item
+		Accordingly, every Reject under Values Equal is a false alarm (\falsealarm),
+		while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
+	\end{itemize}
+	\caption{Case comparison for array type compatibility, given pairs of dimension expressions.
+		TODO: get Peter's LaTeX help on overall appearance, probably including column spacing/centering and bullet indentation.}
+	\label{f:DimexprRuleCompare}
+\end{figure}
+
+
+Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
+It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafely.
+It also shows that C-incompatibilities only occur in cases that C treats unsafely.
+
 
 The conservatism of the new rule set can leave a programmer needing a recourse,
Index: doc/theses/mike_brooks_MMath/uw-ethesis.tex
===================================================================
--- doc/theses/mike_brooks_MMath/uw-ethesis.tex	(revision d3942b9eeb219288b12ece12702144a21189a2b4)
+++ doc/theses/mike_brooks_MMath/uw-ethesis.tex	(revision 42d81a7e47cbd21d6203945bd49cc404cd002be2)
@@ -87,4 +87,5 @@
 \usepackage{graphicx}
 \usepackage{tabularx}
+\usepackage{pifont}
 \usepackage[labelformat=simple,aboveskip=0pt,farskip=0pt,font=normalsize]{subfig}
 \renewcommand\thesubfigure{(\alph{subfigure})}