The AdaCore Blog
An Insight Into the AdaCore Ecosystem
Security Is a Team Sport. Give Your Engineers the Tools to Win.
Gem #153: Multicore Maze Solving, Part 1
Yannick Moy
SPARK 2014 Rationale: Loop Variants
Loop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very…
Yannick Moy
SPARK 2014 Rationale: Loop Invariants
Formal verification tools like GNATprove rely on two main inputs from programmers: subprogram contracts (preconditions and postconditions) and loop…
Gem #152 : Defining a New Language in a Project File
Yannick Moy
SPARK 2014 Rationale: Pre-call and Pre-loop Values
Subprogram contracts are commonly presented as special assertions: the precondition is an assertion checked at subprogram entry, while the…
Yannick Moy
MISRA-C 2012 vs SPARK 2014, the Subset Matching Game
The MISRA C subset of C defines around 150 rules that restrict C programs for critical software development. Of these, 27 rules are classified as…
Florian Schanda
SPARK 2014 Flow Analysis
We have nearly finished implementing a central component of the SPARK 2014 analysis tools: the flow analysis engine; so this is a good time to…
Yannick Moy
SPARK 2014 Rationale: Specification Functions
Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet,…
Johannes Kanig
SPARK 2014 goes to Space!
David Lesens from Astrium was a member of the Hi-Lite project ("was" because the project is finished now, see the previous post), and has tried…
Yannick Moy
SPARK 2014 Rationale: Contract Cases
Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a…
Gem #151 : Specifying Mathematical Properties of Programs