source: doc/theses/mike_brooks_MMath/intro.tex@ bdc8591

\chapter{Introduction}

All modern programming languages provide three high-level containers (collection): array, linked, and string.
Often array is part of the programming language, while linked is built from pointer types, and string from a combination of array and linked.

\cite{Blache19}
\cite{Oorschot23}
\cite{Ruef19}

\section{Array}

Array provides a homogeneous container with $O(1)$ access to elements using subscripting.
The array size can be static, dynamic but fixed after creation, or dynamic and variable after creation.
For static and dynamic-fixed, an array can be stack allocated, while dynamic-variable requires the heap.


\section{Linked List}

Linked provides a homogeneous container with $O(log N)$/$O(N)$ access to elements using successor and predecessor operations.
Subscripting by value is sometimes available.
Linked types are normally dynamically sized by adding/removing node using link fields internal or external to the elements (nodes).
If a programming language allows pointer to stack storage, linked types can be allocated on the stack;
otherwise, elements are heap allocated and explicitly/implicitly managed.


\section{String}

String provides a dynamic array of homogeneous elements, where the elements are often human-readable characters.
What differentiates string from other types in that string operations work on blocks of elements for scanning and changing the elements, rather than accessing individual elements.
Nevertheless, subscripting is often available.
The cost of string operations is less important than the power of the block operation to accomplish complex manipulation.
The dynamic nature of string means storage is normally heap allocated but often implicitly managed, even in unmanaged languages.


\section{C/\CFA}

The goal of this work is to introduce safe and complex versions of array, link, and string into the programming language \CFA, which based on the C.


\subsection{Common knowledge}

The reader is assumed to have used C or \CC for the coursework of at least four university-level courses, or have equivalent experience.
The current discussion introduces facts, unaware of which, such a functioning novice may be operating.

% TODO: decide if I'm also claiming this collection of facts, and test-oriented presentation is a contribution; if so, deal with (not) arguing for its originality

\subsection{Convention: C is more touchable than its standard}

When it comes to explaining how C works, I like illustrating definite program semantics.
I prefer doing so, over a quoting manual's suggested programmer's intuition, or showing how some compiler writers chose to model their problem.
To illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and I show its behaviour.

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
\end{itemize}

The compiler whose program semantics is shown is
\begin{cfa}
$ gcc --version
gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0
\end{cfa}
running on Architecture @x86_64@, with the same environment targeted.

Unless explicit discussion ensues about differences among compilers or with (versions of) the standard, it is further implied that there exists a second version of GCC and some version of Clang, running on and for the same platform, that give substantially similar behaviour.
In this case, I do not argue that my sample of major Linux compilers is doing the right thing with respect to the C standard.


\subsection{C reports many ill-typed expressions as warnings}

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


\section{Contributions}

\subsection{Linked List}

\subsection{Array}

\subsection{String}