Index: doc/theses/mike_brooks_MMath/background.tex
===================================================================
--- doc/theses/mike_brooks_MMath/background.tex	(revision f277ab6c2f5cfddea9d864a3868b6a824a3ba1ef)
+++ doc/theses/mike_brooks_MMath/background.tex	(revision 266732e2818527a06669f666f04fb32c296a3b9f)
@@ -21,14 +21,14 @@
 This behaviour is typically one of
 \begin{itemize}
-    \item my statement that the compiler accepts or rejects the program
-    \item the program's printed output, which I show
-    \item my implied assurance that its assertions do not fail when run
+	\item my statement that the compiler accepts or rejects the program
+	\item the program's printed output, which I show
+	\item my implied assurance that its assertions do not fail when run
 \end{itemize}
 
 The compiler whose program semantics is shown is
-\begin{lstlisting}
+\begin{cfa}
 $ gcc --version
 gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0
-\end{lstlisting}
+\end{cfa}
 running on Architecture @x86_64@, with the same environment targeted.
 
@@ -39,6 +39,32 @@
 \subsection{C reports many ill-typed expressions as warnings}
 
-TODO: typeset
-\lstinputlisting[language=C, firstline=13, lastline=56]{bkgd-c-tyerr.c}
+These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
+\lstinput{12-15}{bkgd-c-tyerr.c}
+with warnings:
+\begin{cfa}
+warning: assignment to 'float *' from incompatible pointer type 'void (*)(void)'
+warning: assignment to 'void (*)(void)' from incompatible pointer type 'float *'
+\end{cfa}
+Similarly,
+\lstinput{17-19}{bkgd-c-tyerr.c}
+with warning:
+\begin{cfa}
+warning: passing argument 1 of 'f' from incompatible pointer type
+note: expected 'void (*)(void)' but argument is of type 'float *'
+\end{cfa}
+with a segmentation fault at runtime.
+
+That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@.
+Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition.
+
+A "tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute"*1 rejected the program.
+The behaviour (whose absence is unprovable) is neither minor nor unlikely.
+The rejection shows that the program is ill-typed.
+
+Yet, the rejection presents as a GCC warning.
+
+In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing.
+
+*1  TAPL-pg1 definition of a type system
 
 
@@ -47,13 +73,94 @@
 \subsection{C has an array type (!)}
 
-TODO: typeset
-\lstinputlisting[language=C, firstline=35, lastline=116]{bkgd-carray-arrty.c}
+When a programmer works with an array, C semantics provide access to a type that is different in every way from ``pointer to its first element.''
+Its qualities become apparent by inspecting the declaration
+\lstinput{34-34}{bkgd-carray-arrty.c}
+The inspection begins by using @sizeof@ to provide definite program semantics for the intuition of an expression's type.
+Assuming a target platform keeps things concrete:
+\lstinput{35-36}{bkgd-carray-arrty.c}
+Consider the sizes of expressions derived from @a@, modified by adding ``pointer to'' and ``first element'' (and including unnecessary parentheses to avoid confusion about precedence).
+\lstinput{37-40}{bkgd-carray-arrty.c}
+That @a@ takes up 40 bytes is common reasoning for C programmers.
+Set aside for a moment the claim that this first assertion is giving information about a type.
+For now, note that an array and a pointer to its first element are, sometimes, different things.
+
+The idea that there is such a thing as a pointer to an array may be surprising.
+It is not the same thing as a pointer to the first element:
+\lstinput{42-45}{bkgd-carray-arrty.c}
+The first gets
+\begin{cfa}
+warning: assignment to `float (*)[10]' from incompatible pointer type `float *'
+\end{cfa}
+and the second gets the opposite.
+
+We now refute a concern that @sizeof(a)@ is reporting on special knowledge from @a@ being an local variable,
+say that it is informing about an allocation, rather than simply a type.
+
+First, recognizing that @sizeof@ has two forms, one operating on an expression, the other on a type, we observe that the original answers are unaffected by using the type-parameterized form:
+\lstinput{46-50}{bkgd-carray-arrty.c}
+Finally, the same sizing is reported when there is no allocation at all, and we launch the analysis instead from the pointer-to-array type.
+\lstinput{51-57}{bkgd-carray-arrty.c}
+So, in spite of considerable programmer success enabled by an understanding that an array just a pointer to its first element (revisited TODO pointer decay), this understanding is simplistic.
+
+A shortened form for declaring local variables exists, provided that length information is given in the initializer:
+\lstinput{59-63}{bkgd-carray-arrty.c}
+In these declarations, the resulting types are both arrays, but their lengths are inferred.
+
+\begin{tabular}{lllllll}
+@float x;@ & $\rightarrow$ & (base element) & @float@ & @float x;@ & @[ float ]@ & @[ float ]@ \\
+@float * x;@ & $\rightarrow$ & pointer & @float *@ & @float * x;@ & @[ * float ]@ & @[ * float ]@ \\
+@float x[10];@ & $\rightarrow$ & array & @float[10]@ & @float x[10];@ & @[ [10] float ]@ & @[ array(float, 10) ]@ \\
+@float *x[10];@ & $\rightarrow$ & array of pointers & @(float*)[10]@ & @float *x[10];@ & @[ [10] * float ]@ & @[ array(*float, 10) ]@ \\
+@float (*x)[10];@ & $\rightarrow$ & pointer to array & @float(*)[10]@ & @float (*x)[10];@ & @[ * [10] float ]@ & @[ * array(float, 10) ]@ \\
+@float *(*x5)[10];@ & $\rightarrow$ & pointer to array & @(float*)(*)[10]@ & @float *(*x)[10];@ & @[ * [10] * float ]@ & @[ * array(*float, 10) ]@
+\end{tabular}
+\begin{cfa}
+	 x5 =	 (float*(*)[10]) x4;
+//	x5 =	 (float(*)[10]) x4;  // wrong target type; meta test suggesting above cast uses correct type
+
+	// [here]
+	// const
+
+	// [later]
+	// static
+	// star as dimension
+	// under pointer decay:				int p1[const 3]  being  int const *p1
+
+	const float * y1;
+	float const * y2;
+	float * const y3;
+
+	y1 = 0;
+	y2 = 0;
+	// y3 = 0; // bad
+
+	// *y1 = 3.14; // bad
+	// *y2 = 3.14; // bad
+	*y3 = 3.14;
+
+	const float z1 = 1.414;
+	float const z2 = 1.414;
+
+	// z1 = 3.14; // bad
+	// z2 = 3.14; // bad
+
+
+}
+
+#define T float
+void stx2() { const T x[10];
+//			x[5] = 3.14; // bad
+			}
+void stx3() { T const x[10];
+//			x[5] = 3.14; // bad
+			}
+\end{cfa}
 
 My contribution is enabled by recognizing
 \begin{itemize}
-    \item There is value in using a type that knows how big the whole thing is.
-    \item The type pointer to (first) element does not.
-    \item C \emph{has} a type that knows the whole picture: array, e.g. @T[10]@.
-    \item This type has all the usual derived forms, which also know the whole picture.  A usefully noteworthy example is pointer to array, e.g. @T(*)[10]@.
+	\item There is value in using a type that knows how big the whole thing is.
+	\item The type pointer to (first) element does not.
+	\item C \emph{has} a type that knows the whole picture: array, e.g. @T[10]@.
+	\item This type has all the usual derived forms, which also know the whole picture.  A usefully noteworthy example is pointer to array, e.g. @T(*)[10]@.
 \end{itemize}
 
@@ -75,7 +182,7 @@
 a declaration is always the type followed by the declared identifier name;
 for the example of letting @x@ be a \emph{pointer to array}, the declaration is spelled:
-\begin{lstlisting}
+\begin{cfa}
 [ * [10] T ] x;
-\end{lstlisting}
+\end{cfa}
 The \CFA-Full column gives the spelling of a different type, introduced in TODO, which has all of my contributed improvements for safety and ergonomics.
 
@@ -83,108 +190,118 @@
 \textbf{Unfortunate Syntactic Reference}
 
-\noindent
+\begin{figure}
+\centering
+\setlength{\tabcolsep}{3pt}
 \begin{tabular}{llllll}
-    & Description & Type & Declaration & \CFA-C  & \CFA-Full \\ \hline
-    $\triangleright$ & val.
-        & @T@ 
-        & @T x;@ 
-        & @[ T ]@
-        & 
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} val.\\ \footnotesize{no writing the val.\ in \lstinline{x}}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T} \\ \lstinline{T const}   }
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x;} \\ \lstinline{T const x;}   }
-        & @[ const T ]@
-        & 
-        \\ \hline
-    $\triangleright$ & ptr.\ to val.
-        & @T *@ 
-        & @T * x;@ 
-        & @[ * T ]@
-        &
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
-        & @T * const@ 
-        & @T * const x;@ 
-        & @[ const * T ]@
-        & 
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x;} \\ \lstinline{T const * x;}   }
-        & @[ * const T ]@
-        & 
-        \\ \hline
-    $\triangleright$ & ar.\ of val.
-        & @T[10]@ 
-        & @T x[10];@ 
-        & @[ [10] T ]@
-        & @[ array(T, 10) ]@
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{x[5]}}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T[10]} \\ \lstinline{T const[10]}   }
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x[10];} \\ \lstinline{T const x[10];}   }
-        & @[ [10] const T ]@
-        & @[ const array(T, 10) ]@
-        \\ \hline
-    & ar.\ of ptr.\ to val.
-        & @T*[10]@
-        & @T *x[10];@
-        & @[ [10] * T ]@
-        & @[ array(* T, 10) ]@
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x[5]}}   }\vspace{2pt}
-        & @T * const [10]@ 
-        & @T * const x[10];@ 
-        & @[ [10] const * T ]@
-        & @[ array(const * T, 10) ]@
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*(x[5])}}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * [10]} \\ \lstinline{T const * [10]}   }
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x[10];} \\ \lstinline{T const * x[10];}   }
-        & @[ [10] * const T ]@
-        & @[ array(* const T, 10) ]@
-        \\ \hline
-    $\triangleright$ & ptr.\ to ar.\ of val.
-        & @T(*)[10]@
-        & @T (*x)[10];@
-        & @[ * [10] T ]@
-        & @[ * array(T, 10) ]@
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
-        & @T(* const)[10]@
-        & @T (* const x)[10];@
-        & @[ const * [10] T ]@
-        & @[ const * array(T, 10) ]@
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{(*x)[5]}}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T(*)[10]} \\ \lstinline{T const (*) [10]}   }
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T (*x)[10];} \\ \lstinline{T const (*x)[10];}   }
-        & @[ * [10] const T ]@
-        & @[ * const array(T, 10) ]@
-        \\ \hline
-    & ptr.\ to ar.\ of ptr.\ to val.
-        & @T*(*)[10]@
-        & @T *(*x)[10];@
-        & @[ * [10] * T ]@
-        & @[ * array(* T, 10) ]@
-        \\ \hline
+	& Description & Type & Declaration & \CFA-C  & \CFA-Full \\ \hline
+	$\triangleright$ & val.
+	    & @T@ 
+	    & @T x;@ 
+	    & @[ T ]@
+	    & 
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} val.\\ \footnotesize{no writing the val.\ in \lstinline{x}}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T} \\ \lstinline{T const}   }
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x;} \\ \lstinline{T const x;}   }
+	    & @[ const T ]@
+	    & 
+	    \\ \hline \hline
+	$\triangleright$ & ptr.\ to val.
+	    & @T *@ 
+	    & @T * x;@ 
+	    & @[ * T ]@
+	    &
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
+	    & @T * const@ 
+	    & @T * const x;@ 
+	    & @[ const * T ]@
+	    & 
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x;} \\ \lstinline{T const * x;}   }
+	    & @[ * const T ]@
+	    & 
+	    \\ \hline \hline
+	$\triangleright$ & ar.\ of val.
+	    & @T[10]@ 
+	    & @T x[10];@ 
+	    & @[ [10] T ]@
+	    & @[ array(T, 10) ]@
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{x[5]}}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T[10]} \\ \lstinline{T const[10]}   }
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x[10];} \\ \lstinline{T const x[10];}   }
+	    & @[ [10] const T ]@
+	    & @[ const array(T, 10) ]@
+	    \\ \hline
+	& ar.\ of ptr.\ to val.
+	    & @T*[10]@
+	    & @T *x[10];@
+	    & @[ [10] * T ]@
+	    & @[ array(* T, 10) ]@
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x[5]}}   }\vspace{2pt}
+	    & @T * const [10]@ 
+	    & @T * const x[10];@ 
+	    & @[ [10] const * T ]@
+	    & @[ array(const * T, 10) ]@
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*(x[5])}}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * [10]} \\ \lstinline{T const * [10]}   }
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x[10];} \\ \lstinline{T const * x[10];}   }
+	    & @[ [10] * const T ]@
+	    & @[ array(* const T, 10) ]@
+	    \\ \hline \hline
+	$\triangleright$ & ptr.\ to ar.\ of val.
+	    & @T(*)[10]@
+	    & @T (*x)[10];@
+	    & @[ * [10] T ]@
+	    & @[ * array(T, 10) ]@
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
+	    & @T(* const)[10]@
+	    & @T (* const x)[10];@
+	    & @[ const * [10] T ]@
+	    & @[ const * array(T, 10) ]@
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{(*x)[5]}}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T(*)[10]} \\ \lstinline{T const (*) [10]}   }
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T (*x)[10];} \\ \lstinline{T const (*x)[10];}   }
+	    & @[ * [10] const T ]@
+	    & @[ * const array(T, 10) ]@
+	    \\ \hline
+	& ptr.\ to ar.\ of ptr.\ to val.
+	    & @T*(*)[10]@
+	    & @T *(*x)[10];@
+	    & @[ * [10] * T ]@
+	    & @[ * array(* T, 10) ]@
+	    \\ \hline
 \end{tabular}
+\caption{Figure}
+\end{figure}
 
 
 \subsection{Arrays decay and pointers diffract}
 
-TODO: typeset
-\lstinputlisting[language=C, firstline=4, lastline=26]{bkgd-carray-decay.c}
-
+The last section established the difference between these four types:
+\lstinput{3-6}{bkgd-carray-decay.c}
+But the expression used for obtaining the pointer to the first element is pedantic.
+The root of all C programmer experience with arrays is the shortcut
+\lstinput{8-8}{bkgd-carray-decay.c}
+which reproduces @pa0@, in type and value:
+\lstinput{9-9}{bkgd-carray-decay.c}
+The validity of this initialization is unsettling, in the context of the facts established in the last section.
+Notably, it initializes name @pa0x@ from expression @a@, when they are not of the same type:
+\lstinput{10-10}{bkgd-carray-decay.c}
 
 So, C provides an implicit conversion from @float[10]@ to @float*@, as described in ARM-6.3.2.1.3:
-
 \begin{quote}
-    Except when it is the operand of the @sizeof@ operator, or the unary @&@ operator, or is a
-    string literal used to initialize an array
-    an expression that has type ``array of type'' is
-    converted to an expression with type ``pointer to type'' that points to the initial element of
-    the array object
+Except when it is the operand of the @sizeof@ operator, or the unary @&@ operator, or is a
+string literal used to initialize an array
+an expression that has type ``array of type'' is
+converted to an expression with type ``pointer to type'' that points to the initial element of
+the array object
 \end{quote}
 
@@ -206,8 +323,8 @@
 leads to an expectation that the runtime handling is uniform across legal and illegal accesses.
 Moreover, consider the common pattern of subscripting on a malloc result:
-\begin{lstlisting}
-    float * fs = malloc( 10 * sizeof(float) );
-    fs[5] = 3.14;
-\end{lstlisting}
+\begin{cfa}
+float * fs = malloc( 10 * sizeof(float) );
+fs[5] = 3.14;
+\end{cfa}
 The @malloc@ behaviour is specified as returning a pointer to ``space for an object whose size is'' as requested (ARM-7.22.3.4.2).
 But program says \emph{nothing} more about this pointer value, that might cause its referent to \emph{be} an array, before doing the subscript.
@@ -229,10 +346,10 @@
 the parameter's type becomes a type that I summarize as being the array-decayed type.
 The respective handlings of the following two parameter spellings shows that the array-spelled one is really, like the other, a pointer.
-\lstinputlisting[language=C, firstline=40, lastline=44]{bkgd-carray-decay.c}
+\lstinput{12-16}{bkgd-carray-decay.c}
 As the @sizeof(x)@ meaning changed, compared with when run on a similarly-spelled local variariable declaration,
 GCC also gives this code the warning: ```sizeof' on array function parameter `x' will return size of `float *'.''
 
 The caller of such a function is left with the reality that a pointer parameter is a pointer, no matter how it's spelled:
-\lstinputlisting[language=C, firstline=60, lastline=63]{bkgd-carray-decay.c}
+\lstinput{18-21}{bkgd-carray-decay.c}
 This fragment gives no warnings.
 
@@ -240,5 +357,5 @@
 Note the opposite meaning of this spelling now, compared with its use in local variable declarations.
 This point of confusion is illustrated in:
-\lstinputlisting[language=C, firstline=80, lastline=87]{bkgd-carray-decay.c}
+\lstinput{23-30}{bkgd-carray-decay.c}
 The basic two meanings, with a syntactic difference helping to distinguish,
 are illustrated in the declarations of @ca@ vs.\ @cp@,
@@ -252,13 +369,12 @@
 In sumary, when a funciton is written with an array-typed parameter,
 \begin{itemize}
-    \item an appearance of passing an array by value is always an incorrect understanding
-    \item a dimension value, if any is present, is ignorred
-    \item pointer decay is forced at the call site and the callee sees the parameter having the decayed type
+	\item an appearance of passing an array by value is always an incorrect understanding
+	\item a dimension value, if any is present, is ignorred
+	\item pointer decay is forced at the call site and the callee sees the parameter having the decayed type
 \end{itemize}
 
 Pointer decay does not affect pointer-to-array types, because these are already pointers, not arrays.
 As a result, a function with a pointer-to-array parameter sees the parameter exactly as the caller does:
-\lstinputlisting[language=C, firstline=100, lastline=110]{bkgd-carray-decay.c}
-
+\lstinput{32-42}{bkgd-carray-decay.c}
 
 \noindent
@@ -268,39 +384,41 @@
 (Parameter declaration; ``no writing'' refers to the callee's ability)
 
-\noindent
+\begin{figure}
+\centering
 \begin{tabular}{llllll}
-    & Description & Type & Param. Decl & \CFA-C  \\ \hline
-    $\triangleright$ & ptr.\ to val.
-        & @T *@ 
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{T * x,} \\ \lstinline{T x[10],} \\ \lstinline{T x[],}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * T ]} \\ \lstinline{[ [10] T ]} \\ \lstinline{[ [] T  ]}   }
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
-        & @T * const@ 
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{T * const x,} \\ \lstinline{T x[const 10],} \\ \lstinline{T x[const],}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{[ const * T ]} \\ \lstinline{[ [const 10] T ]} \\ \lstinline{[ [const] T  ]}   }
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x,} \\ \lstinline{T const * x,} \\ \lstinline{const T x[10],} \\ \lstinline{T const x[10],} \\ \lstinline{const T x[],} \\ \lstinline{T const x[],}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{[* const T]} \\ \lstinline{[ [10] const T ]} \\ \lstinline{[ [] const T  ]}   }
-        \\ \hline
-    $\triangleright$ & ptr.\ to ar.\ of val.
-        & @T(*)[10]@
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{T (*x)[10],} \\ \lstinline{T x[3][10],} \\ \lstinline{T x[][10],}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{[* [10] T]} \\ \lstinline{[ [3] [10] T ]} \\ \lstinline{[ [] [10] T  ]}   }
-        \\ \hline
-    & ptr.\ to ptr.\ to val.
-        & @T **@
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{T ** x,} \\ \lstinline{T *x[10],} \\ \lstinline{T *x[],}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * * T ]} \\ \lstinline{[ [10] * T ]} \\ \lstinline{[ [] * T  ]}   }
-        \\ \hline
-    & \pbox{20cm}{ \vspace{2pt} ptr.\ to ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{**argv}}   }\vspace{2pt}
-        & @const char **@
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{const char *argv[],} \\ \footnotesize{(others elided)}   }\vspace{2pt}
-        & \pbox{20cm}{ \vspace{2pt} \lstinline{[ [] * const char ]} \\ \footnotesize{(others elided)}   }
-        \\ \hline
+	& Description & Type & Param. Decl & \CFA-C  \\ \hline
+	$\triangleright$ & ptr.\ to val.
+	    & @T *@ 
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{T * x,} \\ \lstinline{T x[10],} \\ \lstinline{T x[],}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * T ]} \\ \lstinline{[ [10] T ]} \\ \lstinline{[ [] T  ]}   }
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
+	    & @T * const@ 
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{T * const x,} \\ \lstinline{T x[const 10],} \\ \lstinline{T x[const],}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{[ const * T ]} \\ \lstinline{[ [const 10] T ]} \\ \lstinline{[ [const] T  ]}   }
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x,} \\ \lstinline{T const * x,} \\ \lstinline{const T x[10],} \\ \lstinline{T const x[10],} \\ \lstinline{const T x[],} \\ \lstinline{T const x[],}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{[* const T]} \\ \lstinline{[ [10] const T ]} \\ \lstinline{[ [] const T  ]}   }
+	    \\ \hline \hline
+	$\triangleright$ & ptr.\ to ar.\ of val.
+	    & @T(*)[10]@
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{T (*x)[10],} \\ \lstinline{T x[3][10],} \\ \lstinline{T x[][10],}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{[* [10] T]} \\ \lstinline{[ [3] [10] T ]} \\ \lstinline{[ [] [10] T  ]}   }
+	    \\ \hline
+	& ptr.\ to ptr.\ to val.
+	    & @T **@
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{T ** x,} \\ \lstinline{T *x[10],} \\ \lstinline{T *x[],}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * * T ]} \\ \lstinline{[ [10] * T ]} \\ \lstinline{[ [] * T  ]}   }
+	    \\ \hline
+	& \pbox{20cm}{ \vspace{2pt} ptr.\ to ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{**argv}}   }\vspace{2pt}
+	    & @const char **@
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{const char *argv[],} \\ \footnotesize{(others elided)}   }\vspace{2pt}
+	    & \pbox{20cm}{ \vspace{2pt} \lstinline{[ [] * const char ]} \\ \footnotesize{(others elided)}   }
+	    \\ \hline
 \end{tabular}
-
+\caption{Figure}
+\end{figure}
 
 
@@ -309,30 +427,26 @@
 When the desired number of elements is unknown at compile time,
 a variable-length array is a solution:
-\begin{lstlisting}
-    int main( int argc, const char *argv[] ) {
-
-        assert( argc == 2 );
-        size_t n = atol( argv[1] );
-        assert( 0 < n && n < 1000 );
-
-        float a[n];
-        float b[10];
-
-        // ... discussion continues here
-    }
-\end{lstlisting}
-This arrangement allocates @n@ elements on the @main@ stack frame for @a@,
-just as it puts 10 elements on the @main@ stack frame for @b@.
+\begin{cfa}
+int main( int argc, const char *argv[] ) {
+	assert( argc == 2 );
+	size_t n = atol( argv[1] );
+	assert( 0 < n && n < 1000 );
+
+	float a[n];
+	float b[10];
+
+	// ... discussion continues here
+}
+\end{cfa}
+This arrangement allocates @n@ elements on the @main@ stack frame for @a@, just as it puts 10 elements on the @main@ stack frame for @b@.
 The variable-sized allocation of @a@ is provided by @alloca@.
 
-In a situation where the array sizes are not known to be small enough
-for stack allocation to be sensible,
-corresponding heap allocations are achievable as:
-\begin{lstlisting}
-    float *ax1 = malloc( sizeof( float[n] ) );
-    float *ax2 = malloc( n * sizeof( float ) );
-    float *bx1 = malloc( sizeof( float[1000000] ) );
-    float *bx2 = malloc( 1000000 * sizeof( float ) );
-\end{lstlisting}
+In a situation where the array sizes are not known to be small enough for stack allocation to be sensible, corresponding heap allocations are achievable as:
+\begin{cfa}
+float *ax1 = malloc( sizeof( float[n] ) );
+float *ax2 = malloc( n * sizeof( float ) );
+float *bx1 = malloc( sizeof( float[1000000] ) );
+float *bx2 = malloc( 1000000 * sizeof( float ) );
+\end{cfa}
 
 
@@ -353,6 +467,5 @@
 Just as an array's element type can be @float@, so can it be @float[10]@.
 
-While any of @float*@, @float[10]@ and @float(*)[10]@ are easy to tell apart from @float@,
-telling them apart from each other may need occasional reference back to TODO intro section.
+While any of @float*@, @float[10]@ and @float(*)[10]@ are easy to tell apart from @float@, telling them apart from each other may need occasional reference back to TODO intro section.
 The sentence derived by wrapping each type in @-[3]@ follows.
 
@@ -360,19 +473,14 @@
 telling them apart from each other is what it takes to know what ``array of arrays'' really means.
 
-
 Pointer decay affects the outermost array only
 
-
 TODO: unfortunate syntactic reference with these cases:
 
 \begin{itemize}
-    \item ar. of ar. of val (be sure about ordering of dimensions when the declaration is dropped)
-    \item ptr. to ar. of ar. of val
+	\item ar. of ar. of val (be sure about ordering of dimensions when the declaration is dropped)
+	\item ptr. to ar. of ar. of val
 \end{itemize}
 
 
-
-
-
 \subsection{Arrays are (but) almost values}
 
@@ -391,6 +499,4 @@
 
 \subsection{Returning an array is (but) almost possible}
-
-
 
 
@@ -414,17 +520,17 @@
 which type information associated with a polymorphic return type
 replaces @malloc@'s use of programmer-supplied size information.
-\begin{lstlisting}
-    // C, library
-    void * malloc( size_t );
-    // C, user
-    struct tm * el1 = malloc(      sizeof(struct tm) );
-    struct tm * ar1 = malloc( 10 * sizeof(struct tm) );
-
-    // CFA, library
-    forall( T * ) T * alloc();
-    // CFA, user
-    tm * el2 = alloc();
-    tm (*ar2)[10] = alloc();
-\end{lstlisting}
+\begin{cfa}
+// C, library
+void * malloc( size_t );
+// C, user
+struct tm * el1 = malloc(      sizeof(struct tm) );
+struct tm * ar1 = malloc( 10 * sizeof(struct tm) );
+
+// CFA, library
+forall( T * ) T * alloc();
+// CFA, user
+tm * el2 = alloc();
+tm (*ar2)[10] = alloc();
+\end{cfa}
 The alloc polymorphic return compiles into a hidden parameter, which receives a compiler-generated argument.
 This compiler's argument generation uses type information from the left-hand side of the initialization to obtain the intended type.
@@ -436,13 +542,13 @@
 In the last example, the choice of ``pointer to array'' @ar2@ breaks a parallel with @ar1@.
 They are not subscripted in the same way.
-\begin{lstlisting}
-    ar1[5];
-    (*ar2)[5];
-\end{lstlisting}
+\begin{cfa}
+ar1[5];
+(*ar2)[5];
+\end{cfa}
 Using ``reference to array'' works at resolving this issue.  TODO: discuss connection with Doug-Lea \CC proposal.
-\begin{lstlisting}
-    tm (&ar3)[10] = *alloc();
-    ar3[5];
-\end{lstlisting}
+\begin{cfa}
+tm (&ar3)[10] = *alloc();
+ar3[5];
+\end{cfa}
 The implicit size communication to @alloc@ still works in the same ways as for @ar2@.
 
@@ -453,7 +559,6 @@
 where the type requested is an array, making the result, much more obviously, an array object.
 
-The ``reference to array'' type has its sore spots too.  TODO see also @dimexpr-match-c/REFPARAM_CALL (under TRY_BUG_1)@
-
-
+The ``reference to array'' type has its sore spots too.
+TODO see also @dimexpr-match-c/REFPARAM_CALL@ (under @TRY_BUG_1@)
 
 TODO: I fixed a bug associated with using an array as a T.  I think.  Did I really?  What was the bug?
