SPARK 2014: Why I am backing a predictable winner
In a recent posting, Embedded.com technical editor Bernard Cole compared the C programming language to a prize-winning race horse: temperamental, stubborn, and unpredictable
These are not the qualities that you would choose for a programming language you intend to deploy for a high-integrity embedded system, where safety or security are key requirements. In this context, we want languages that offer predictability and an efficient and effective means of automated verification.
The SPARK programming language, as described in previous postings was specifically designed with the goals of predictability and verifiability in mind. One of the key concepts embodied in SPARK is that of a contract: a statement of intended functionality by a designer which has to be met by the implementer and can be automatically checked by support tools.
As a result of their success in the field of program verification, contracts have now been absorbed into Ada - the mainstream language of which SPARK is a contractualised subset. Ada 2012 – the most recent version of the language – now contains a native syntax for functional contracts expressed as Pre and Post “Aspects.” Accordingly, the next generation of the SPARK language, called SPARK 2014 , will switch from using structured comments for contracts to using the built-in Ada 2012 equivalents.
There are two ways to understand Pre- and Postconditions in SPARK 2014: as a form of run-time assertion (‘executable semantics’) or as formal specification statements giving a ‘mathematical semantics’ against which an implementation can be proved correct.
Run-time assertions are a paradigm that will be familiar to users of other imperative programming languages such as C. They express a condition that we expect to hold true whilst a program is running and hence can be used as a form of defensive programming: if the condition is false then program execution is halted.
Ada allows programmers to explicitly include assertions in the body of a subprogram and Ada 2012 goes further than this. When the compiler encounters a Precondition on the specification of a subprogram then it will include an assertion as the first statement to be executed when the subprogram is called.
You can think of it as placing an obligation on anyone calling a subprogram to make sure that the condition will be true. For example, if you are going to call a subprogram to push another value onto a stack, you ought to make sure before you call it that the stack isn’t already full. This can be captured by a precondition attached to the declaration of the Push subprogram.
Similarly, the compiler will (with the right switches enabled) translate a postcondition into a run time assertion that is the last statement executed in a subprogram. So if we capture in a postcondition what our stack should look like after a new value has been Pushed then an assert statement will be executed to check that the subprogram has achieved the desired effect each time it is called.
Already this is a very powerful tool for a programmer, but SPARK 2014 takes this one step further by adding the mathematical view of the pre- and postconditions. In this scenario, we can use proof tools to automatically check that programs are going to fulfil the contracts specified in their specs. And proving means that we can check this statically ie. pre-compile, pre-execution, and we can do it for all possible executions – not just the ones we test.
So having written functional contracts for our program, we can choose how to verify the implementation against them. This could be by proof, by testing, or by a combination of the two – so-called Hybrid Verification.
In this approach, the SPARK 2014 verification toolset can by applied to automatically prove that the implementation is correct and free from run-time exceptions. Only where proof cannot be completed automatically is it necessary to write unit tests - with the same contracts used to specify the expected outcome of the tests.
In addition to the pre- and postcondition contracts offered in the base language, SPARK 2014 will use the aspect notation of Ada 2012 to strengthen the specification capabilities of the language by the addition of contracts for:
- Global data dependencies,
- Information flows,
- State abstraction, and
- Data and behaviour refinement
When it comes to choosing a programming language, I’m backing SPARK 2014 to deliver the predictable behaviour needed for the next generation of embedded and critical systems. To keep in touch with developments and for further information about the SPARK 2014 language and toolset, visit www.spark-2014.org.
Stuart Matthews is a Chartered Engineer with 18 years post-doctorate experience with one of the UK’s leading software companies, Altran UK, and a software tools start-up, High Integrity Solutions. Stuart specialises in the design and verification of high-integrity and safety-critical systems and is currently Product Manager for the SPARK technology at Altran.