We've hosted last week in Paris a meeting of the SPARK team for discussing features that will go in SPARK 16.0, and starting planning beyond that. The good news is that support for tasking is well under way, and that it should be completed in time for SPARK 16.0 in Q1 of 2016. For more details about this support, see the corresponding chapter of the SPARK Reference Manual. Except that, we've discussed the other major features in SPARK 16.0 on which we're currently working:
- Generation of counter-examples is starting to work. So you can get values of variables which trigger a failure when a check (a run-time check or an assertion) may fail. We have integrated this feature in GPS, so that a user can in one click display the values from the counter-example interspersed with lines of code.
- As we're now shipping Z3 as a third prover in SPARK (Alt-Ergo was the original prover used in SPARK, and CVC4 was added last year), the current default choice to enable all provers (until recently Alt-Ergo and CVC4) starts to be costly for a first analysis of a code, in which we expect many checks to be unprovable. We're leaning towards a faster default (just one prover), with an easy way to increase proof power towards full power, meaning using all provers, a more costly proof strategy and a large timeout for each proof.
- We have started work to benefit from dedicated prover support for floating-point arithmetic. Z3 currently provides such a support, and Martin Brain from CVC4 team is giving us access to the branch on which he develops this support for CVC4. Initial experiments are very satisfying, so we hope to include such an initial improved support for floats in SPARK Pro 16.0
- As we increase the number of sources for proving properties, it becomes even more important to provide a synthetic view of everything that was proved and by which tool. This global proof summary is being finalized now.
- We will work on fixing the support for Object Orientation in GNATprove as soon as the GNAT compiler will implement the new semantics of calls in class-wide preconditions and postconditions (decided during a meeting of the Ada Rapporteur Group in late 2014). This impacts in particular proofs that a derived class implements only behaviors allowed in the parent class (a.k.a. Liskov Substitution Principle). The implementation in GNAT is under way.
- We had noticed some time ago a bottleneck when running GNATprove on very large projects. We have now identified and fixed the source of the bottleneck, and a pre-analysis which took 130mn on a very large project now takes 1mn on that project. This should also benefit smaller projects of course.
We also discussed two important features that will not make it in SPARK 16.0, but on which we'd like to start working asap for future releases:
- Using the static analysis engine of our CodePeer tool inside GNATprove will provide a valuable new source of proofs, for properties that may be hard to prove with SMT provers (like Alt-Ergo, CVC4 and Z3). For example, CodePeer is quite good at propagating bounds of variables along subprogram paths, which will allow it to prove some run-time checks that may be much more costly or even unprovable with SMT provers. We have discussed how CodePeer needs to be adapted to fit the constraints of this new usage.
- In some cases, flow analysis in GNATprove is not sufficient to prove initialiation of data and non-aliasing of parameters. In such cases, we'd like to hand over the difficult properties to provers, instead of issuing potential false alarms. A typical example is the initialization of an array in a loop, which currently leads to false alarms being issued by GNATprove. This is a feature we're considering now for releases after SPARK 16.0
We were all quite happy about the meeting, as you can see in this picture:
[left to right: Stuart Matthews (Altran), Angela Wallenburg (Altran), Anthony Leonardo Gracio (AdaCore), Johannes Kanig (AdaCore), Clément Fumex (Inria), Claire Dross (AdaCore), Steve Baird (AdaCore), Yannick Moy (AdaCore), Florian Schanda (Altran)]
Not everyone in the team was on the picture, but that's a good subset!