AdaCore Blog

An Insight Into the AdaCore Ecosystem

by Yannick Moy –

GNATprove Tips and Tricks: How to Write Loop Invariants

Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants are necessary for various loops, we detail here a methodology for how users can come up with the right loop invariants for their loops. This methodology in four steps allows users to progressively add the necessary information in their loop invariants, with the tool GNATprove providing the required feedback at each step on whether the information provided is sufficient or not.

#Formal Verification    #SPARK   

by Yannick Moy –

Case Study for System to Software Integrity Includes SPARK 2014

My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.

#Formal Verification    #Certification    #SPARK   

by Yannick Moy –

Muen Separation Kernel Written in SPARK

The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been proved free from run-time errors. This project is part of the secure multilevel workstation project by Secunet, a German security company, which is using SPARK and Isabelle to create the next generation of secure workstations providing different levels of security to government employees and military personnel. I present why I think this project is worth following closely.

#Language    #Formal Verification    #SPARK   

by 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 input values in the postcondition, using the Old attribute. Unfortunately, these rules also make it difficult to express some complex postconditions that may be useful when doing formal verification. In this post, I describe how contract cases allow the expression of these complex contracts, while still detecting potential problems with uses of the Old attribute.

#Language    #Formal Verification    #SPARK   

by 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, sequences of modifications may be illegal, etc. SPARK 2014 provides a way to define abstractly the global state of a unit, so that it can be referred to in subprogram specifications. The associated toolset checks correct access to global variables in the implementation.

#Language    #Formal Verification    #SPARK   

by 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 useful at first, they can prove effective as I show with a simple binary search example. And we came up with both an elegant syntax and a slick refinement for loop variants in SPARK 2014, compared to similar constructs in other languages.

#Language    #Formal Verification    #SPARK   

by 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 invariants. While the first ones are easy to understand (based on the "contract" analogy, in which a subprogram and its caller have mutual obligations), the second ones are not so simple to grasp. This post presents loop invariants and the choices we made in SPARK 2014.

#Language    #Formal Verification    #SPARK   

by 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 postcondition is an assertion checked at subprogram exit. A subtlety not covered by this simplified presentation is that postconditions are really two-state assertions: they assert properties over values at subprogram exit and values at subprogram entry. A special attribute Old is defined in Ada 2012 to support these special assertions. A special attribute Loop_Entry is defined in SPARK 2014 to support similar special assertions for loops.

#Formal Verification    #SPARK