[SystemSafety] Correctness by construction: Godelian oddities

[Olwen Morgan]

Here is a simple program in C. On the assumption that the integer 
representation is 1C, 2C, or SM (I can't recall using a compiler that 
doesn't use one of those three), it prints 0 if plain char is unsigned 
and something negative if it is signed, according to what the integer 
representation is:


#include<stdio.h>

int main(void)
{
     char ch = 0;

     ch = ~(ch^ch);

     printf("%i\n", (int)ch);

     return 0;

}

The only way a C verifier can prove what this program will print is for 
it to be told  *a priori* somewhere in its configuration parameters what 
the integer representation is - which is here what the program is 
designed to reveal, i.e. the functional requirement that it satisfies is 
to produce a value that permits discrimination among 1C, 2C, and SM 
representations. Otherwise, AFAI can see, the best a verifier could do 
would be to say that the output is either 0 or the relevant negative value.

One gets an even weirder program by omitting the initialisation of the 
variable ch and putting the call to printf in the return statement - 
which breaks all kinds of SPARK-like rules:


#include<stdio.h>

int main(void)
{
     char ch;

     return printf("%i\n", (int)(~(ch^ch)));

}

According to the C standard, the access to ch in the call to printf will 
produce undefined results because ch has never been initialised. In my 
tests clang-4.0.0 warned of an uninitialised variable at compile time 
but gcc 5.4.0 did not. Nevertheless, even if the storage used for ch has 
unpredictable contents, the value will still be some bit pattern and the 
expression "~(ch^ch) will set the bits to all ones, thereby producing 
(under 1C, 2C, or SM) a defined value. Thus, although a verifier might 
warn of undefinedness, it is possible in some circumstances for the 
program to produce a result that is unambiguously defined for the 
purposes of determining the representation of the char type. Indeed, I 
do not know of any C compiler that, AFAI recall, would generate code 
that would bomb out or produce a result other than 0 or the relevant 
negative value. What an interpreter might do with it is anybody's guess 
but then the way an interpreter handles a program is closer how a 
verifier handles it.

Anyone got any apt names for this kind of situation? AFAI can see it's 
not a case of a long-span requirement. Perhaps one might call them 
"Gödelian oddities"?


Olwen