14 entries written by Yannick Moy
Just a few weeks ago, one of our partners reported a strange behavior of the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file. When the last line of the file was of a specific length like 499 or 500 or 1000, and not terminated with a newline character, then Get_Line raised an exception End_Error instead of returning the expected string. That was puzzling for a central piece of code known to have worked for the past 10 years! But fair enough, there was indeed a bug in the interaction between subprograms in this code, in boundary cases having to do with the size of an intermediate buffer. My colleague Ed Schonberg who fixed the code of Get_Line had nonetheless the intuition that this particular event, finding such a bug in an otherwise trusted legacy piece of code, deserved a more in depth investigation to ensure no other bugs were hiding. So he challenged the SPARK team at AdaCore in checking the correctness of the patched version. He did well, as in the process we uncovered 3 more bugs.
The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.
If you're somewhat interested in formal methods applied to software, but you never had the chance to really look at it, now is the time! Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College have written a truly essential book for getting up to speed with formal verification using SPARK. I really love this book, and here are the aspects I love most:
Project Hi-Lite started in 2010 with the objective of making it cost-effective to use formal verification instead of testing for critical software. Just a few months before, Airbus had presented their five “must-have” criteria for adopting a formal method: soundness, applicability to the code, usability by “normal” engineers on “normal” computers, improve on classical methods, certifiability. We have had these five criteria very much in mind during these three years, and here are the results for SPARK 2014 and the associated tool GNATprove.