The guarantees provided by SPARK, an open-source formal proof tool for Ada, and its analysis are only as strong as the properties that were initially specified. In particular, use of third-party libraries or the Ada standard libraries may weaken the analysis, if the relevant properties of the library API are not specified. We progressively added contracts to some of the GCC GNAT Ada standard libraries to enable users to prove additional properties when using them, thus increasing the safety of their programs. In this talk, I will present the different levels of insurance those contracts can provide, from preventing some run-time errors to occur, to describing entirely their action.
Speakers: Joffrey Huguet