49 entries tagged with #Ada 2012
by Yannick Moy , Claire Dross

Proving the Correctness of GNAT Light Runtime Library
The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use at the highest levels of criticality in several industrial domains. It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations. We have used SPARK to prove the correctness of 40 of them: that the code is free of runtime errors, and that it satisfies its functional specifications.by Jessie Glockner
Celebrating Women Engineering Heroes - International Women in Engineering Day 2021
Women make up roughly 38% of the global workforce, yet they constitute only 10–20% of the engineering workforce. In the U.S., numbers suggest that 40% of women who graduate with engineering degrees never enter the profession or eventually leave it. Why? The reasons vary but primarily involve socio-economic constraints on women in general, workplace inequities, and lack of support for work-life balance. Sadly, history itself has often failed to properly acknowledge the instrumental contributions of women inventors, scientists, and mathematicians who have helped solve some of our world's toughest challenges. How can young women emulate their successes if they don't even know about them?
by Roderick Chapman
Performance analysis and tuning of SPARKNaCl
This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.by Arnaud Charlet
Ada 202x support in GNAT
News from the Ada front The next revision of the Ada standard is now almost ready, so it's time for a status update on where GNAT and AdaCore stand on this front!
by Pierre-Marie de Rodat
Introducing source code instrumentation in GNATcoverage
This is the first post of a series about GNATcoverage and source code instrumentation.In order to make GNATcoverage viable in more contexts, we planned several years ago to add instrumentation support in GNATcoverage for Ada sources. This feature reached maturation recently and is available in the last Continuous Release, so it is a good time to present it with a blog series!by Jessie Glockner , Ben Brosgol
The FACE™ open systems strategy gaining traction in the avionics industry
The FACE™ approach is a government-industry initiative for reducing defense system life cycle costs through portable and reusable software components. It consists of a technical approach — a software standard based on well-defined common interfaces — and a business strategy for encouraging the development and deployment of FACE conformant products.by Emma Adby

Make with Ada 2020: The SmartBase - IoT Adjustable Bed
John Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed lighting! Additionally, this project won first place prize in the 2019/20 Make with Ada competition.by Abe Cohen
An Introduction to Contract-Based Programming in Ada
One of the most powerful features of Ada 2012* is the ability to specify contracts on your code. Contracts describe conditions that must be satisfied upon entry (preconditions) and upon exit (postconditions) of your subprogram. Preconditions describe the context in which the subprogram must be called, and postconditions describe conditions that will be adhered to by the subprogram’s implementation. If you think about it, contracts are a natural evolution of Ada’s core design principle. To encourage developers to be as explicit as possible with their expressions, putting both the compiler/toolchain and other developers in the best position to help them develop better code.
by Paul Butcher
AdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems
What's changed?In 2019 AdaCore created a UK business unit and embarked on a new and collaborative venture researching and developing advanced UK aerospace systems. This blog introduces the reader to ‘HICLASS’, describes our involvement and explains how participation in this project is aligned with AdaCore’s core values.
by Michael Frank
Learning SPARK via Conway's Game of Life
How I learned to write SPARK-provable code using Conway's Game Of Lifeby Juan Zamorano
Using Ada for a Spanish Satellite Project
I am an Associate Professor at Polytechnic University of Madrid’s (Universidad Politécnica de Madrid / UPM) in the Department of Architecture and Technology of Computer Systems. For the past several years I have been directing a team of colleagues and students in the development of a UPMSat-2 microsatellite. The project originally started in 2013 as a follow-to the UPM-SAT 1, launched by an Ariane-4 in 1995.
by Claire Dross
Using Pointers in SPARK
In this blog post, I will present one of the most interesting additions to the community 2019 version of SPARK: pointer support. One of the core assumption in SPARK has always been the absence of aliasing, so adding pointers without breaking this assumption was quite a challenge. I will explain how this was achieved using an ownership model for pointers (like is done in Rust) through small examples.by Pamela Trevino
Public Ada Training Paris June 3-7, 2019
This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.
by Yannick Moy , Nicolas Setton , Ben Brosgol
A Readable Introduction to Both MISRA C and SPARK Ada
MISRA C is the most widely known coding standard restricting the use of the C programming language for critical software. For good reasons. For one, its focus is entirely on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. In addition, a large majority of rules it defines are checkable automatically (116 rules out of the total 159 guidelines), and many tools are available to enforce those. As a coding standard, MISRA C even goes out of its way to define a consistent sub-language of C, with its own typing rules (called the "essential type model" in MISRA C) to make up for the lack of strong typing in C.
by Pamela Trevino
Public Ada Training Paris, France Dec 3 - 7, 2018
This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.
by Julia Teissl

Train control using Ada on a Raspberry Pi
I was looking for a topic for my master thesis in embedded systems engineering when one of my advisor proposed the idea of programming a control system for autonomous trains in Ada. Since I am fascinated by the idea of autonomous vehicles I agreed immediately without knowing Ada.
by Rob Tice
SPARKZumo Part 1: Ada and SPARK on Any Platform
So you want to use SPARK for your next microcontroller project? Great choice! All you need is an Ada 2012 ready compiler and the SPARK tools. But what happens when an Ada 2012 compiler isn’t available for your architecture?
by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2
This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing with C, error handling, memory management, and loading functions.by Felix Krause

The Road to a Thick OpenGL Binding for Ada: Part 1
This blog post is part one of a tutorial based on the OpenGLAda project and will cover some the background of the OpenGL API and the basic steps involved in importing platform-dependent C functions.
by J. German Rivera

Make with Ada 2017- A "Swiss Army Knife" Watch
SummaryThe Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor. This blog article describes the development of a "Swiss Army Knife" watch on the Hexiwear platform. It is a bare-metal embedded application developed 100% in Ada 2012, from the lowest level device drivers all the way up to the application-specific code, for the Hexiwear's K64F microcontroller. I developed Ada drivers for Hexiwear-specific peripherals from scratch, as they were not supported by AdaCore's Ada drivers library. Also, since I wanted to use the GNAT GPL 2017 Ada compiler but the GNAT GPL distribution did not include a port of the Ada Runtime for the Hexiwear board, I also had to port the GNAT GPL 2017 Ada runtime to the Hexiwear. All this application-independent code can be leveraged by anyone interested in developing Ada applications for the Hexiwear wearable device.
by Yannick Moy , Martin Becker , Emanuel Regnath
Physical Units Pass the Generic Test
The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue has been mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci who introduced special aspects for specifying physical dimensions on types. This dimension system did not attempt to deal with generics though. As was noted by others, handling generics in a dimensional analysis that is, like in GNAT, a compile-time analysis with no impact on the executable size or running time, is the source of the problem of dimension handling. Together with our partners from Technical Universitat München, we have finally solved this remaining difficulty.by Emmanuel Briot
User-friendly strings API
User friendly strings APIIn a previous post, we described the design of a new strings package, with improved performance compared to the standard Ada unbounded strings implementation. That post focused on various programming techniques used to make that package as fast as possible.
by Pat Rogers
Getting started with the Ada Drivers Library device drivers
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
by AdaCore Admin
Make With Ada Winners Announced!
Judging for the first annual Make with Ada competition has come to an end and we can now reveal the results.
by Claire Dross
SPARK 2014 Rationale: Support for Type Invariants
Type invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation. Type invariant are part of Ada 2012 but were not supported in SPARK until SPARK Pro 17.by Quentin Ochem

Unity & Ada
Using Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.by AdaCore Admin

VectorCAST/Ada: Ada 2012 Language Support
We are pleased to announce that on April 27th our partner, Vector, will host a webinar to showcase their latest VectorCAST/Ada release!
by AdaCore Admin

Provably safe programming at Embedded World
AdaCore continues to build reliable and secure software for embedded software development tools. Last month, we attended Embedded World 2016, one of the largest conferences of its kind in Europe, to present our embedded solutions and our expertise for safety, and mission critical applications in a variety of domains.
by AdaCore Admin
Formal Verification Made Easy!
We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.
by Maxim Reznik , Nicolas Setton
Using reference types to handle persistent objects
The Ada 2012 standard introduced user-defined references. The main idea behind this is simplifying the access to elements in a container. But you can use them to control the life-circle of your persistent objects. Let's see how it could work.
by AdaCore Admin

AdaCore Tech Days 2015
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 Yannick Moy
SPARK 2014 Rationale: Type Predicates
Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.by Fabien Chouteau

Make with Ada: "The Eagle has landed"
July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?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 Emmanuel Briot
Larger than it looks (storage pools)
This post shows how to implement a special storage pool that allocates an extra header every time it allocates some memory. This can be used to store type specific information, outside of the type itself.by Jamie Ayre

20 years on...
20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions
by Olivier Ramonat

AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0
February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.
by Johannes Kanig
Testing, Static Analysis, and Formal Verification
I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).
by Tristan Gingold , Yannick Moy

Tetris in SPARK on ARM Cortex M4
Tetris is a well-known game from the 80's, which has been ported in many versions to all game platforms since then. There are even versions of Tetris written in Ada. But there was no version of Tetris written in SPARK, so we've repaired that injustice. Also, there was no version of Tetris for the Atmel SAM4S ARM processor, another injustice we've repaired.
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.by Yannick Moy
