AdaCore Blog

13 entries tagged with #Containers

by Pierre-Marie de Rodat

Pretty-Printing Ada Containers with GDB Scripts

When things don’t work as expected, developers usually do one of two things: either add debug prints to their programs, or run their programs under a debugger. Today we’ll focus on the latter activity.

#gdb   

by Fabien Chouteau

Ada on the first RISC-V microcontroller

Updated July 2018

#Embedded Development    #Ada    #RISC-V   

by Claire Dross

Quantifying over Elements of a Container

Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain. The way quantified formulas over containers are translated for proof can be tuned in GNATprove using a specific annotation.

#Formal Verification    #SPARK   

by Florian Schanda

SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I

Today I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features, I intend to focus on the how I have proved absence of run-time errors in the name table and lexer. I had two objectives: show absence of run-time errors, and do not write useless defensive code. Today's blog will be about the name table, a data structure found in many compilers that can map strings to a unique integer and back. The next blog post will talk about the lexical analyzer.

#Dev Projects    #Formal Verification    #SPARK   

by Yannick Moy

SPARK Prez at New Conference on Railway Systems

RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.

#SPARK   

by Emmanuel Briot

Traits-Based Containers

This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.

#Ada    #Containers    #Generics   

by Emmanuel Briot

Count them all (reference counting)

Reference countingReference counting is a way to automatically reclaim unused memory. An element is automatically deallocated as soon as there are no more references to it in the program.

#Ada    #memory management    #Storage Pools   

by Yannick Moy

Using SPARK to Prove AoRTE in Robot Navigation Software

Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that even NASA has not solved it. Researchers have used SPARK to do precisely that for 3 well-known robot navigation algorithms. Their results will be presented at the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September.

#Formal Verification    #SPARK    #Robotics   

by Claire Dross

External Axiomatizations: a Trip Into SPARK’s Internals

There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the mathematical world, like trigonometry functions), cumbersome (especially if they require concepts that cannot easily be described using contracts, like transitivity, counting, summation...), or simply inefficient, for big and complex data structures like containers for example. In these cases, a user can provide directly a manually written Why3 translation for an Ada package using a feature named external axiomatizations. Coming up with this manual translation requires both a knowledge of the WhyML language and a minimal understanding of GNATprove's mechanisms and is therefore reserved to advanced users.

#Formal Verification    #SPARK   

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 Claire Dross

SPARK 2014 Rationale: Verifying Properties over Formal Containers

We saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how these properties can be verified by the proof tool called GNATprove.

#Language    #Formal Verification    #SPARK   

by Claire Dross

SPARK 2014 Rationale: Expressing Properties over Formal Containers

We saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of these containers, using quantified expressions.

#Language    #Formal Verification    #SPARK   

by Claire Dross

SPARK 2014 Rationale: Formal Containers

SPARK 2014 excludes data structures based on pointers. Instead, one can use the library of formal containers. They are variant of the Ada 2012 bounded containers, specifically designed and annotated to facilitate the proof of programs using them.

#Language    #Formal Verification    #SPARK