The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...
Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.
I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!
A new course on university.adacore.com presents the SPARK language and tools. The first lecture is now online, and others will follow this year.
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.
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!