SPARK 16 will contain a better way to see a summary of the verification results. This blog post introduces the new feature.
Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.
The international team developing the SPARK product, usually dispersed across continents and islands (if UK still counts as an Island despite the Channel Tunnel), has gathered the last week of June to discuss the progress towards SPARK Pro 16.0, and beyond that. Here are the main points that we discussed.
It is with great sadness that I have to announce the death of Robert Dewar. Robert was President of AdaCore, and he has had a tremendous influence on the development of SPARK.
by Pavlos Efstathopoulos in – June 26, 2015
Constants whose initial expressions depend on global variables or formal parameters can now appear in flow-related contracts. This allows more accurate specification and verification of information flow properties.
The annual release of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, the changes are quite noticeable, with much improved provability, automation and usability. I know some people have been waiting for it for many months, so here it is!
Floating point problems are difficult and interesting. This blog post describes the process of creating floating point benchmarks: one of the activities are doing to help out the SMTLIB effort (SMTLIB is the language our VCs are expressed in).
In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous 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, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.
Our intern Anthony Leonardo Gracio has rewritten the code of the stabilization system of the Crazyflie drone, initially written in C, and verified with GNATprove that the code is free from run-time errors. Read all about it on AdaCore's blog.
Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.