[SystemSafety] C for OSs

[David Crocker]

Roderick, shame on you for writing in C! A small subset of C++ is vastly
superior. You get encapsulation, a stronger type system, and generics.
With generics you can define your own array types (or use std::array if
it meets your requirements) and bounded string types. You can also
define your own range-limited scalar types (or with eCv/eCv++ you have
the constrained typedef in the language already).

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

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