In 2010, Rod Chapman, then technical leader of the SPARK team at Altran, released an implementation in SPARK of the Skein cryptographic hash algorithm. Using the previous version of the SPARK technology, Rod proved that his implementation was free of run-time errors (even found a subtle corne-case bug in the C reference implementation), but that was no trivial task, as he explained later in a paper surveying past projects in SPARK:

The proofs of type safety turned out to be quite tricky. Firstly, finding the correct loop invariants proved difficult, and this was compounded by the plethora of modular types and non-linear arithmetic in the VC structures. Of the 367 VCs, 23 required use of the Checker to complete the proof - not bad but these still required a substantial effort to complete.

Considering that Rod is a leading expert in the technology, that assessment alone could deter non-expert users from ever attempting a similar project!

Now comes SPARK 2014 and the new version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology:

• In his 2010 paper, Rod wrote: "The 344 automatically discharged proofs were harder (and slower) than expected. This owes to the prevalence of "modulo B" arithmetic in the VCs". With the improved support for bitwise operations in GNATprove, all these proofs go through automatically without any user involvment.
• Rod also wrote: "The main problem is finding a sufficiently strong precondition of loop invariant for the offending code." The problem lies with the amount of supporting contracts and assertions that one must write, most of it in the form of contracts on internal subprograms and loop invariants. Counting each conjunct in a conjunction of properties (A and B and ...) as one element, we can compare the effort Rod put in the initial version and the effort we put in the new SPARK 2014 version:
  • The initial version had 35 precondition elements on internal subprograms. The new version has 18.
  • The initial version had 26 postcondition elements on internal subprograms. The new version has 4.
  • The initial version had 43 loop invariant elements. The new version has 7.
  • The initial version had 24 cut elements (special assertions that summarize execution paths). The new version has none.
  • The initial version had 22 hint elements (assertions used to ease the work of automatic provers). The new version has none.

Overall, the previous toolset required 150 supporting specification elements to be written to prove absence of run-time errors in a program specified with 18 visible contract elements (preconditions and postconditions of visible subprograms), which amounts to 11% of useful specification elements. With the new SPARK technology, one only requires 29 supporting specification elements to prove a program with 22 visible contract elements, which amounts to 43% of useful specification elements. So we've gone from 1 out of 10 specifications being useful to almost half of them.

If you're curious about the advances in the technology that made this possible, you can read the section on 'sparkskein' in the SPARK User's Guide which gives more details.