[SystemSafety] C for OSs

[Olwen Morgan]

I'm not sure that's what I would regard as a first-class Boolean type.

And, anyway, I tend AFAP to stick to C90 on my usual paranoid-critical 
grounds.

Olwen


On 09/09/2019 12:03, David Crocker wrote:
>
> C does have a first-class Boolean type since the 1999 version. Sadly, 
> it's type-convertible to integer; but any MISRA-C checker will take 
> care of that.
>
> David Crocker, Escher Technologies Ltd.
> http://www.eschertech.com
> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
> On 09/09/2019 11:13, Olwen Morgan wrote:
>>
>>
>> I agree with your point about different compilers. It's a hefty 
>> challenge for any C tool developer to come up with retrofitted formal 
>> semantics that fit many compilers.
>>
>> As regards the lack of features in C, again I agree. AFAI recall QAC 
>> can produce diagnostics that make up for the lack of named type 
>> equivalence. Functions can make up to a significant extent for the 
>> lack of first-class Boolean and array types. One can program around 
>> the lack of user-defined scalar types. But of course, C simply does 
>> not have packages.
>>
>> But for all the possibility of workarounds, they remain just that. It 
>> takes effort to give yourself anything approaching the convenience of 
>> Ada's superior language design.
>>
>> Your comment about an acceptable false-positive rate is illuminating. 
>> Very early in my use of QAC, I simply decided to live with a high 
>> false-positive rate as the price of getting good diagnostics. Only 
>> gradually did I reduce the false positives by adopting the 
>> paranoid-critical C programming style that I use today - and here the 
>> surrealist overtones are not entirely frivolous.
>>
>> For the avoidance of doubt, _IMO yo__u _*_c_**_annot 
>> _**_equal_*_SPARK Ada code quality in C_. I've only ever said that 
>> you can approach it (albeit, I'm confident, fairly closely) by using 
>> different best-of-breed tools and exercising a severe coding 
>> discipline that takes a long time - and perhaps a peculiar mindset - 
>> to acquire.
>>
>> And all that hassle really shouldn't be necessary in the first place.
>>
>> Olwen
>>
>>
>> On 09/09/2019 10:29, Roderick Chapman wrote:
>>>
>>> On 08/09/2019 18:23, Olwen Morgan wrote:
>>>> Rod Chapman and I have a long-standing (and exceedingly civilised 
>>>> :-) difference of opinion in this area. If you have the right 
>>>> tools, and if you are prepared to observe draconian coding 
>>>> discipline, then I believe that you can in C approach a SPARK Ada 
>>>> level of code quality. Rod, if I am not traducing him, has 
>>>> lingering doubts about this. IMO tools are no longer the problem 
>>>> since those who write them simply retrofit sensible formal 
>>>> semantics to (annotation-extended subsets of) C and then perform 
>>>> verifications accordingly.
>>>
>>> I still have reservations. The big challenge is to come up with a 
>>> formal semantics that is implemented by both your favourite 
>>> verification tool and all versions of all compilers that you might 
>>> have to use during the lifetime of a project. If you can "lock in" 
>>> to exactly ONE compiler, then things are significantly simpler... 
>>> but this is not a good place to be when, in twenty years time, you 
>>> really do have to change compiler for a hardware update or some 
>>> other reason, but the vendor has long since gone out of business. I 
>>> see far too many projects stuck in this particular rut.
>>>
>>> In SPARK, it works by the complete removal of undefined behaviours 
>>> and any dependence on unspecified behaviour. This requires 
>>> subsetting and forms of analysis, which you need to be demonstrably 
>>> sound and efficient enough to scale up to large programs.
>>>
>>> I am currently engaged in writing some highly critical C code, using 
>>> the latest Frama-C toolset. I find the experience rather 
>>> frustrating... the problem seems to be two-fold:
>>>
>>> 1. C is lacking some fundamental features that make SPARK work. (The 
>>> short version: user-defined scalar types, named type equivalence, a 
>>> first-class Boolean type, packages, formal parameter modes, and 
>>> first-class array types).
>>>
>>> 2. Some very basic things in C are undefined. Worst-offender: signed 
>>> integer overflow.
>>>
>>> The upshot is that I find it's very hard to get to an acceptable 
>>> false-positive rate from the Frama-C WP tool. On a recent SPARK 
>>> project, the "acceptable" false alarm rate for type-safety proof was 
>>> ZERO.. so perhaps my expectations are set too high?
>>>
>>> Example: in SPARK, we use user-defined scalar types all over the 
>>> place to describe invariants from the problem domain which apply to 
>>> every parameter, constant and variable of each type. That info is 
>>> used by the VC generator to constrain the values of variables, so 
>>> that proving non-overflow becomes tractable. I don't know how to do 
>>> that in C... (if anyone does know how, please help me out...)
>>>
>>>  - Rod
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> The System Safety Mailing List
>>> systemsafety at TechFak.Uni-Bielefeld.DE
>>> Manage your subscription: 
>>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190909/9f147587/attachment.html>