Blog

Yannick Moy

GNATprove Tips and Tricks: Referring to Input in Contracts

In a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to…

Yannick Moy

SPARK 2014 Rationale: Global State

Global variables are a common source of programming errors: they may fail to be initialized properly, they can be modified in unexpected ways,…

Gem #154: Multicore Maze Solving, Part 2

Yannick Moy

SPARK 2014 Rationale: Mixing SPARK and Ada Code

The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification…

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,…