Index: doc/theses/mike_brooks_MMath/intro.tex =================================================================== --- doc/theses/mike_brooks_MMath/intro.tex (revision 82e5670b382ce297cad720a0ac24ccb659cdb8f1) +++ doc/theses/mike_brooks_MMath/intro.tex (revision 6a8c7733a0906dffced0ff8356128c785ad992f2) @@ -33,43 +33,33 @@ -\section{C/\CFA} +\section{Motivation} -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. +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 C. +Unfortunately, to make C better while retaining a high level of backwards compatibility requires a significant knowledge of C's design. +Hence, it is assumed the reader has a medium knowledge of C or \CC, on which extensive new C knowledge is built. -\subsection{Common knowledge} +\subsection{C?} -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 +Like many established programming languages, C has a standards committee and multiple ANSI/ISO language manuals~\cite{C99,C11,C18,C23}. +However, most programming languages are only partially explained by these manuals. +When it comes to explaining how C works, the definitive source is the @gcc@ compiler, which is mimicked by other C compilers, such as Clang~\cite{clang}. +Often other C compilers must \emph{ape} @gcc@ because a large part of the C library (runtime) system is embedded with @gcc@ features. +While some key aspects of C need to be explained by quoting from the language reference manual, to illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and shows its behaviour. +These example programs show \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 the compiler accepts or rejects certain syntax, + \item the prints output to buttress a claim of behaviour, + \item executes without triggering any embedded assertions testing pre/post-assertions or invariants. \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. +This work has been tested across @gcc@ versions 8--12 and clang version 10 running on ARM, AMD, and Intel architectures. +Any discovered anomalies among compilers or versions is discussed. 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} +\subsection{Ill-Typed Expressions} -These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed. +C reports many ill-typed expressions as warnings. +For example, these attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed. \lstinput{12-15}{bkgd-c-tyerr.c} with warnings: @@ -86,17 +76,18 @@ \end{cfa} with a segmentation fault at runtime. +Clearly, @gcc@ understands these ill-typed case, and yet allows the program to compile, which seems like madness. +Compiling with @-Werror@, which turns warnings into errors, is often too strong, because some warnings are just warnings. +In the following discussion, ``ill-typed'' means giving a nonzero @gcc@ exit condition with a message that discusses typing. +Note, \CFA's type-system rejects all these ill-typed cases as type mismatch errors. -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. +% 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 +% 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. +% *1 TAPL-pg1 definition of a type system