Changeset 6a8c773 for doc/theses


Ignore:
Timestamp:
Mar 24, 2024, 11:08:46 PM (9 months ago)
Author:
Peter A. Buhr <pabuhr@…>
Branches:
master
Children:
41fb996
Parents:
82e5670
Message:

more work on introduction

File:
1 edited

Legend:

Unmodified
Added
Removed

  • doc/theses/mike_brooks_MMath/intro.tex

    r82e5670 r6a8c773  
    3333
    3434
    35 \section{C/\CFA}
     35\section{Motivation}
    3636
    37 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.
     37The 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.
     38Unfortunately, to make C better while retaining a high level of backwards compatibility requires a significant knowledge of C's design.
     39Hence, it is assumed the reader has a medium knowledge of C or \CC, on which extensive new C knowledge is built.
    3840
    3941
    40 \subsection{Common knowledge}
     42\subsection{C?}
    4143
    42 The reader is assumed to have used C or \CC for the coursework of at least four university-level courses, or have equivalent experience.
    43 The current discussion introduces facts, unaware of which, such a functioning novice may be operating.
    44 
    45 % 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
    46 
    47 \subsection{Convention: C is more touchable than its standard}
    48 
    49 When it comes to explaining how C works, I like illustrating definite program semantics.
    50 I prefer doing so, over a quoting manual's suggested programmer's intuition, or showing how some compiler writers chose to model their problem.
    51 To illustrate definite program semantics, I devise a program, whose behaviour exercises the point at issue, and I show its behaviour.
    52 
    53 This behaviour is typically one of
     44Like many established programming languages, C has a standards committee and multiple ANSI/ISO language manuals~\cite{C99,C11,C18,C23}.
     45However, most programming languages are only partially explained by these manuals.
     46When 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}.
     47Often other C compilers must \emph{ape} @gcc@ because a large part of the C library (runtime) system is embedded with @gcc@ features.
     48While 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.
     49These example programs show
    5450\begin{itemize}
    55         \item my statement that the compiler accepts or rejects the program
    56         \item the program's printed output, which I show
    57         \item my implied assurance that its assertions do not fail when run
     51        \item the compiler accepts or rejects certain syntax,
     52        \item the prints output to buttress a claim of behaviour,
     53        \item executes without triggering any embedded assertions testing pre/post-assertions or invariants.
    5854\end{itemize}
    59 
    60 The compiler whose program semantics is shown is
    61 \begin{cfa}
    62 $ gcc --version
    63 gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0
    64 \end{cfa}
    65 running on Architecture @x86_64@, with the same environment targeted.
    66 
    67 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.
     55This work has been tested across @gcc@ versions 8--12 and clang version 10 running on ARM, AMD, and Intel architectures.
     56Any discovered anomalies among compilers or versions is discussed.
    6857In this case, I do not argue that my sample of major Linux compilers is doing the right thing with respect to the C standard.
    6958
    7059
    71 \subsection{C reports many ill-typed expressions as warnings}
     60\subsection{Ill-Typed Expressions}
    7261
    73 These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
     62C reports many ill-typed expressions as warnings.
     63For example, these attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
    7464\lstinput{12-15}{bkgd-c-tyerr.c}
    7565with warnings:
    … …  
    8676\end{cfa}
    8777with a segmentation fault at runtime.
     78Clearly, @gcc@ understands these ill-typed case, and yet allows the program to compile, which seems like madness.
     79Compiling with @-Werror@, which turns warnings into errors, is often too strong, because some warnings are just warnings.
     80In the following discussion, ``ill-typed'' means giving a nonzero @gcc@ exit condition with a message that discusses typing.
     81Note, \CFA's type-system rejects all these ill-typed cases as type mismatch errors.
    8882
    89 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@.
    90 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.
     83% 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@.
     84% 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.
    9185
    92 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.
    93 The behaviour (whose absence is unprovable) is neither minor nor unlikely.
    94 The rejection shows that the program is ill-typed.
    95 
    96 Yet, the rejection presents as a GCC warning.
    97 
    98 In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing.
    99 
    100 *1  TAPL-pg1 definition of a type system
     86% 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.
     87% The behaviour (whose absence is unprovable) is neither minor nor unlikely.
     88% The rejection shows that the program is ill-typed.
     89%
     90% Yet, the rejection presents as a GCC warning.
     91% *1  TAPL-pg1 definition of a type system
    10192
    10293
Note: See TracChangeset for help on using the changeset viewer.