21 entries tagged with #Containers
We are thrilled to announce the launch of our highly anticipated course, "Advanced Journey with Ada: A Flight in Progress," which explores the advanced concepts of Ada programming. This course serves as a seamless continuation of our esteemed "Introduction to Ada" course.
A few months ago I was reading this article about coroutines in game development and how they are great tools for writing scripts (as in movie scripts) in the same language as the game engine. Until then I heard about coroutines but never really gave them a thought, this piqued my curiosity.
Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.
Manuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/SPARK and how he created the spark_unbound library
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:
Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!
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.
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.
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.
Updated July 2018
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.