[SystemSafety] Correctness by construction: Godelian oddities

[Olwen Morgan]

On 14/07/2020 07:48, david.haworth at elektrobit.com wrote:
> In the first program, any verifier worth its salt would complain at least
> once (quite aside from the use of stdio), because bitwise operations
> have (unspecified) implementation defined and undefined aspects (C99)
> and char might be either signed or unsigned.

Indeed. The QAC static checker moans prolifically about this sort of 
thing. But it is, in fact, a very controlled use of unspecified 
behaviour (or it would be if I'd got it right - see below). The C99 
definitions of the bitwise operators actually say what the effect on the 
bit patterns is. What is unspecified is what the corresponding resulting 
value is in the case of signed operands. The use of bitwise operators in 
the first example will produce all ones in ch (though whether this is 
stored as all-ones is unspecified - it may be stored as all zeros in 1C 
representation).

BIG CONFESSION: I SCREWED THIS ONE UP ...AARGH !!! .... Derek Jones 
will, *quite rightly*, never let me forget it ... :-)).

What I posted was an out-of-context fragment of a larger program that 
subsequently checks the different possible values to discriminate 
between 1C, 2C, and Sm representations. In a 1 C representation , this 
will not tell you whether ch is signed or unsigned. In fact, I should 
have used an alternating patterns of 0s, and 1s instead of setting 
things all to 1. I'll post a correct version later on.

But the *principle* is the same. You put a controlled bit-pattern with a 
MSB of 1 into a plain char and then check whether it is negative. This 
kind of controlled use of unspecified aspects of program behaviour is 
typically used by compiler testers to determine by testing what the 
implementation-defined and unspecified aspects of a C implementation 
actually are.

> MISRA (for all its warts and blemishes) ...

For which I beseech the Gods to forgive me.

<snip>

> If I were a competent compiler author, I'd be tempted to write
> such a compiler that produces random results every time a construct with
> undefined or implementation-defined is used. Any takers?  :-)

You're certainly not the first to have mulled that one over. :-))


Olwen



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200714/17596b4e/attachment.html>