[SystemSafety] C for OSs

[Roderick Chapman]

On 16/09/2019 09:27, Martyn Thomas wrote:
>
> For programming (in a subset of C++, though the principles are 
> universal), /Elements of Programming/, by Alexander Stepanov and Paul 
> McJones (ISBN 0-321-63537-X)
>
> For project planning and the management of risk and quality: 
> /Strategies for Software Engineering/ by Martyn Ould (ISBN 0-471-92628-0)
>
> The first of these should quickly deter anyone who isn't willing to do 
> the work necessary to write programs that merit the term /engineering/.
>
You're not kidding... Stepanov's "EOP" book is a tough read... it's core 
message is great - bringing a purely formal approach to generic/template 
programming by placing really strong contracts the formal parameters of 
a generic module.  Fantastic so far... but I have 2 problems with it...

1. In late 2012 (when I first read it), it quickly became apparent that 
there was _no_ tool support at all for this "Concepts" based generic 
programming.  We designed something similar in SPARK2005 back in the day 
(it never got finished unfortunately), and it requires a theorem-prover 
of some sophistication to verify that generic instantiations really are 
OK. Doing that with an acceptable compilation speed and false positive 
rate will be quite a trick.  I note that the "Concepts" feature is 
working its way through WG21 for C++ 2X, and some vendors are claiming 
to have implemented it (See 
https://devblogs.microsoft.com/cppblog/c20-concepts-are-here-in-visual-studio-2019-version-16-3/ 
for example.) Is the current C++ Concepts feature exactly what was in 
EOP, or has it changed?

2. On page 46, the authors refine a mathematical specification for 
computing the n'th Fibonacci number into C++ code, and they silently 
ignore the issue of undefined behaviour on signed integer overflow.  
(See their example code, about line 565 in eop.h ... )

If you compile their code with gcc -fsanitize=undefined, and ask for the 
92nd then 93rd Fibonacci number, then you get:

92
fibonacci(92) == 7540113804746346429
93
eop.h:566:30: runtime error: signed integer overflow: 
8828119010029072385 + 3372041405092804353 cannot be represented in type 
'long long int'
fibonacci(93) == -6246583658587674878

Oh dear.

  - Rod



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190916/31f14a71/attachment-0001.html>