by Fabien Chouteau , Nicolas Setton
GNAT Community 2021 is here!
We are happy to announce that the GNAT Community 2021 release is now available via https://www.adacore.com/download. Here are some release highlights:
17 entries tagged with #Containers
by Léo Germond
How To: GNAT Pro with Docker
Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!
by Pat Rogers
From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks
This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.by Allan Ascanius , Per Dalgas Jakobsen
Winning DTU RoboCup with Ada and SPARK
The Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D printed robot with wheel suspension, based on the BeagleBone Blue ARM-based board and the Pixy 1 camera with custom firmware enabling real-time line detection. Code is written in Ada and formally proved correct with SPARK at Silver level.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.
by Fabien Chouteau
Ada on the first RISC-V microcontroller
Updated July 2018
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.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.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.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.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.
by Yannick Moy
