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

[David Crocker]

On 24/10/2018 13:00, Martyn Thomas wrote:
> Yes, people make mistakes and inspections and testing find too few of
> them. That's why you need languages with semantics for which tools can
> be written that detect many such mistakes.
That is entirely possible for C and for most (perhaps all) of C++. I
agree that it's easier in Ada, especially since function contracts
became part of the language. Unfortunately, the number of C and C++
programmers/organisations who are interested in proving their programs
correct seems to be vanishingly small, which is why I have mothballed my
formal verification tools for C and C++.
> For example, if your tools can tell you "this program can generate a
> value for that array index that will be out of bounds", you have the
> opportunity to eliminate the error before it kills someone.
Static analysers for C and C++ seem to be getting quite good at doing
that. Also, we're starting to see static analysis like features creeping
into C++ compiler, as I found out recently when I upgraded to a newer
version of gcc and it promptly reported a bug in a third-party library I
was using. I expect this trend to continue, because of the large overlap
between code optimisation and static analysis.

Personally, I would never use C for safety critical work because it's
lacking major safety features, in particular encapsulation and generics,
and because C++ subsets provide better type safety than C.

- David

>
> Martyn
>
>
> On 24/10/2018 12:11, Derek M Jones wrote:
>> I practice most developers don't read the language standard
>> and most coding mistakes are unrelated to developer knowledge
>> of language semantics, e.g., they are oversights, off
>> by one errors or cut-and-paste slip-ups.
>
>
>
> _______________________________________________
> 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/20181025/68f8b6d2/attachment.html>