[SystemSafety] A small taste of what we're up against

[Olwen Morgan]

@Martyn:

 >>> "Support destructive testing of software ! " ?? I'd say "Support

 >>> programming languages with unambiguous semantics. "

 >>> I'd like to see an ALARP argument for software written in C. Does 
anyone

 >>> have one to share?

With you all the way on that one!

There are, perhaps, some fall-back positions. A former colleague once 
said to me that you have two choices in standardisation: Either you 
standardise a thing itself or you standardise the way it has to be 
described. In C standardisation meetings, I have advocated the addition 
of an Annex to the ISO C standard that at least prescribes how 
implementation-specific features are to be described. Even so modest a 
proposal as that seems anathema to the C standardisation community. And 
in any case, since C has no formal semantics, it is indeed locking the 
stable door after the horse is long gone.

As regards ALARP in C, my view is that you need a subset of draconian 
severity backed up by a subset enforcer tool and then use either an 
abstract interpretation tool or a theorem-prover to show freedom from 
run-time errors. If you go about that the right way, e.g. by using QAC 
and AbsInt (the commercial version of Astree), then I think you can 
approach SPARK Ada levels of confidence. (Rod Chapman and I have had 
(very civilised) professional differences on that one.) The trouble is 
the severity of the subset you have to work with, which apparently 
offends most C coders. You hit a cultural brick wall with it.

@Thierry Coq:

>>> I'd say "support programming languges with unambiguous and easy-to-read semantics"

There are tradeoffs here, even for people who are comfortable with mathematical semantics. What we need is precision with clarity. Denotational semantics are not exactly light bedtime reading. All too often natural-language clarity itself is lacking. It's interesting to compare the first C standard with the first Pascal standard. The languages are broadly comparable except that C has a bigger standard library. Brian Wichmann and Tony Sale, who did most of the original drafting of the Pascal standard, accomplished a tour-de-force. It's still one of the most clearly-worded language standards in existence even after nearly 40 years. One deeply disappointing thing I notice in the burgeoning plethora of unstandardised languages is that some people now don't even use BNF to  describe language syntax.

IMO the C standard could be less than half its current size (750 pages) if more discipline were used in writing it. Unfortunately (and I won't apologise to former colonists here) C standardisation is dominated by Americans who simply cannot write clear, concise technical English. If we cannot get clarity in natural language, there's no point in trying to formalise it. It would be building on sand.

Finally, in case any Yanks here bridle at my disparaging sentiments, I offer the following example from an American crime documentary that I recently watched:

US Police officer:"Ultimately the cadaver was located by a canine unit" (18 syllables)

Translation into English: "In the end a dog found the corpse." (8 syllables)

I've not yet seen an American crime documentary that speaks of "dogs". 
They are always, "canine units" or, at best, "canines" ... WTF? .. Is it 
any wonder that they screw up programming language standards?


Ever ranting against alehorses,

Olwen




On 24/10/2018 10:26, Martyn Thomas wrote:
>
> Martyn
>
>
> On 24/10/2018 08:13, Olwen Morgan wrote:
>> Just a quickie:
>>
>> if, in the code below, you replace:
>>
>>
>>      PrintEvalOrder((a[0]=++i), (a[1]=++i), (a[2]=++i));
>>
>> with:
>>
>>
>>      PrintEvalOrder((++i), (++i), (++i));
>>
>> both clang and tcc tell you the order of evaluation is p1, p2, p3
>> whereas gcc says it's p3, p3, p3. ... WTF?
>>
>> Presumably, this is due to over-zealous optimisation,
>>
>>
>> Support destructive testing of software !
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181024/4455556a/attachment-0001.html>