Changeset b195498 for doc/theses/mike_brooks_MMath/array.tex

Timestamp:

Apr 24, 2025, 6:35:41 PM (5 months ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

6b33e89, f85de47

Parents:

f632bd50

Message:

proofreading intro and background chapters, capitalize section titles, update backtick calls to regular calls

File:

• doc/theses/mike_brooks_MMath/array.tex (modified) (13 diffs)

doc/theses/mike_brooks_MMath/array.tex

@@ -90 +90 @@
 
 
-\section{Dependent typing}
+\section{Dependent Typing}
 
 General dependent typing allows the type system to encode arbitrary predicates (\eg behavioural specifications for functions),
@@ -103 +103 @@
 
 
-\section{Features added}
+\section{Features Added}
 
 This section shows more about using the \CFA array and dimension parameters, demonstrating their syntax and semantics by way of motivating examples.
@@ -782 +782 @@
 
 
-Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
+\VRef[Figure]{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 unsafe.
 It also shows that C-incompatibilities only occur in cases that C treats unsafe.
@@ -859 +859 @@
 
 
-\section{Multidimensional array implementation}
+\section{Multidimensional Array Implementation}
 \label{s:ArrayMdImpl}
 
@@ -978 +978 @@
 \end{figure}
 
-Figure~\ref{fig:subscr-all} shows one element (in the shaded band) accessed two different ways: as @x[2][3]@ and as @x[all][3][2]@.
+\VRef[Figure]{fig:subscr-all} shows one element (in the shaded band) accessed two different ways: as @x[2][3]@ and as @x[all][3][2]@.
 In both cases, value 2 selects from the coarser dimension (rows of @x@),
 while the value 3 selects from the finer dimension (columns of @x@).
@@ -1024 +1024 @@
 % The choice to implement this style-1 system upon C's style-2 arrays, rather than its style-3 pointer arithmetic, reduces the attack surface of unsafe code.
 % My casting is unsafe, but I do not do any pointer arithmetic.
-% When a programmer works in the common-case style-2 subset (in the no-@[all]@ top of Figure~\ref{fig:subscr-all}), my casts are identities, and the C compiler is doing its usual displacement calculations.
+% When a programmer works in the common-case style-2 subset (in the no-@[all]@ top of \VRef[Figure]{fig:subscr-all}), my casts are identities, and the C compiler is doing its usual displacement calculations.
 % If I had implemented my system upon style-3 pointer arithmetic, then this common case would be circumventing C's battle-hardened displacement calculations in favour of my own.
 
@@ -1067 +1067 @@
 
 
-\section{Bound checks, added and removed}
+\section{Bound Checks, Added and Removed}
 
 \CFA array subscripting is protected with runtime bound checks.
@@ -1089 +1089 @@
 
 
-\section{Array lifecycle}
+\section{Array Lifecycle}
 
 An array is an aggregate, like a structure;
@@ -1341 +1341 @@
 % note to Mike, I have more fragments on some details available in push24\fragments\uNoCtor.txt
 
-\section{Comparison with other arrays}
+\section{Comparison with Other Arrays}
 
 
@@ -1457 +1457 @@
 
 
-\subsection{Levels of dependently typed arrays}
+\subsection{Levels of Dependently Typed Arrays}
 
 The \CFA array and the field of ``array language'' comparators all leverage dependent types to improve on the expressiveness over C and Java, accommodating examples such as:
@@ -1504 +1504 @@
 Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.
 
-\subsection{Static safety in C extensions}
-
-
-\section{Future work}
-
-\subsection{Declaration syntax}
-
-\subsection{Range slicing}
-
-\subsection{With a module system}
-
-\subsection{With described enumerations}
+\subsection{Static Safety in C Extensions}
+
+
+\section{Future Work}
+
+\subsection{Declaration Syntax}
+
+\subsection{Range Slicing}
+
+\subsection{With a Module System}
+
+\subsection{With Described Enumerations}
 
 A project in \CFA's current portfolio will improve enumerations.
@@ -1602 +1602 @@
 In the case of adapting this pattern to \CFA, my current work provides an adapter from ``successively subscripted'' to ``subscripted by tuple,'' so it is likely that generalizing my adapter beyond ``subscripted by @ptrdiff_t@'' is sufficient to make a user-provided adapter unnecessary.
 
-\subsection{Retire pointer arithmetic}
+\subsection{Retire Pointer Arithmetic}
 
 
@@ -1614 +1614 @@
 (For later:  That's what I offer with array.hfa, but in the future-work vision for arrays, the fix includes helping programmers stop accidentally using a broken C-ism.)
 
-\subsection{\CFA features interacting with arrays}
+\subsection{\CFA Features Interacting with Arrays}
 
 Prior work on \CFA included making C arrays, as used in C code from the wild,