AdaCore Blog

73 entries tagged with #GNAT

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 Fabien Chouteau

Ada on FPGAs with PicoRV32

When I bought the TinyFPGA-BX board, I thought it would be an opportunity to play a little bit with FPGA, learn some Verilog or VHDL. But when I discovered that it was possible to have a RISC-V CPU on it, I knew I had to run Ada code on it.

#embedded    #RISC-V    #Ada   

by Emma Adby, Fabien Chouteau

GNAT Community 2018 is here!

Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download

by Thomas Quinot

PolyORB now lives on Github

PolyORB, AdaCore's versatile distribution middleware, now lives on Github. Its new home is https://github.com/AdaCore/polyorb

by Rob Tice

SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPS

This is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to automate the process in GPS.

#GPS    #Python    #Libadalang    #Arduino    #CCG   

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?

#CCG    #SPARK    #Arduino    #RISC V    #embedded   

by Fabien Chouteau

Ada on the micro:bit

Updated July 2018

#embedded    #Ada    #nRF51    #ARM   

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.

#OpenGL    #Binding   

by Johannes Kanig

Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto

Bitcoin is getting a lot of press recently, but let's be honest, that's mostly because a single bitcoin worth 800 USD in January 2017 was worth almost 20,000 USD in December 2017. However, bitcoin and its underlying blockchain are beautiful technologies that are worth a closer look. Let’s take that look with our Ada hat on!

#Bitcoin    #Blockchain    #Ada   

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.

#OpenGL    #Binding   

by Lionel Matias

Leveraging Ada Run-Time Checks with Fuzz Testing in AFL

Fuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software component, and wait for it to crash. If, like me, you find writing robustness test tedious and not very efficient in finding bugs, you might want to try fuzzing your Ada code. Here's a recipe to fuzz-test your Ada code, using American Fuzzy Lop and all the runtime checks your favorite Ada compiler can provide. Let's see (quickly) how AFL works, then jump right into fuzzing 3 open-source Ada libraries: ZipAda, AdaYaml, and GNATCOLL.JSON.

#Testing    #Ada    #VerificationTools   

by Manuel Iglesias Abbatermarco

Make with Ada 2017- Ada Based IoT Framework

Summary The Ada IoT Stack consists of an lwIp (“lightweight IP”) stack implementation written in Ada, with an associated high-level protocol to support embedded device connectivity nodes for today’s IoT world. The project was developed for the Make With Ada 2017 competition based on existing libraries and ported to embedded STM32 devices.

#embedded    #Ada    #IoT   

by Jamie Ayre

Welcoming New Members to the GNAT Pro Family

As we see the importance of software grow in applications, the quality of that software has become more and more important. Even outside the mission- and safety-critical arena customers are no longer accepting software failures (the famous blue screens of death, and there are many...). Ada has a very strong answer here and we are seeing more and more interest in using the language from a range of industries. It is for this reason that we have completed our product line by including an entry-level offer for C/C++ developers wanting to switch to Ada and reinforced our existing offer with GNAT Pro Assurance for programmers building the most robust software platforms with life cycles spanning decades.

#GNAT Pro    #Ada   

by Fabien Chouteau

There's a mini-RTOS in my language

The first thing that struck me when I started to learn about the Ada programing language was the tasking support. In Ada, creating tasks, synchronizing them, sharing access to resources, are part of the language

#Ada    #Ravenscar    #embedded    #STM32   

by J. German Rivera

Make with Ada 2017- A "Swiss Army Knife" Watch

Summary  The 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.

#GNAT     #typing   

by Yannick Moy

Prove in the Cloud

We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now experiment live with SPARK without installing first the toolset. Something particularly interesting for academics is that all the code for this widget is open source. So you can setup your own proof server for hands-on sessions, with your own exercises, in a matter of minutes.

#SPARK   

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 Yannick Moy

Research Corner - Focused Certification of SPARK in Coq

The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more complex properties. But the SPARK toolset being itself a complex tool, it is not free of errors. To get confidence in its results, we have worked with academic partners to establish mathematical evidence of the correctness of a critical part of the SPARK toolset. The part on which we focused is the tagging of nodes requiring run-time checks by the frontend of the SPARK technology. This work has been accepted at SEFM 2017 conference.

#SPARK   

by Rob Tice

The Adaroombot Project

The Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it focuses on a control algorithm and a simple serial communications protocol. The iRobot CreateⓇ 2 platform was originally design for STEM education and has great documentation and support - making it very easy to create a control application using Ada. This blog looks at the creation of the project and some cool features of Ada that were learned along the way.

#Raspberry Pi    #ARM    #Linux    #Ada    #Roomba   

by Pierre-Marie de Rodat, Nicolas Setton

GNAT GPL 2017 is out!

For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.

#GNAT GPL   

by Fabien Chouteau

Ada on the first RISC-V microcontroller

Updated July 2018

#Embedded Development    #Ada    #RISC-V   

by Yannick Moy

(Many) More Low Hanging Bugs

We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.

#Static Analysis    #Libadalang   

by Yannick Moy, Nicolas Roche

A Usable Copy-Paste Detector in A Few Lines of Python

After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a copy-paste detector based on Libadalang. It turned out to be both easier than anticipated, and much more efficient and effective than we could have hoped for. In the end, we hope to use this new detector to refactor the codebase of some of our tools, and we expect to integrate it in our IDEs.

#Libadalang    #Static Analysis    #refactoring   

by Emmanuel Briot

User-friendly strings API

User friendly strings API In 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.

#Ada    #gnatcoll   

by Emmanuel Briot

New strings package in GNATCOLL

This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.

#gnatcoll    #strings    #Ada   

by Jerome Guitton, Jérôme Lambourg, Joel Brobecker

Simics helps run 60 000 GNAT Pro tests in 24 hours

This post has been updated in March 2017 and was originally posted in March 2016.

#Simics    #WindRiver    #GNAT Pro   

by Pierre-Marie de Rodat

GNATcoverage moves to GitHub

Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage

#GitHub    #GNATcoverage   

by Jorge Real

Writing on Air

While searching for motivating projects for students of the Real-Time Systems course here at Universitat Politècnica de València, we found a curious device that produces a fascinating effect. It holds a 12 cm bar from its bottom and makes it swing, like an upside-down pendulum, at a frequency of nearly 9 Hz. The free end of the bar holds a row of eight LEDs. With careful and timely switching of those LEDs, and due to visual persistence, it creates the illusion of text... floating in the air!

#STM32    #Ravenscar    #Ada    #Makers    #Embedded Development   

by Fabien Chouteau, Arnaud Charlet, Yannick Moy

SPARK Tetris on the Arduboy

One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered  the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.

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.

#Ada    #Devices    #drivers    #STM32    #embedded   

by Raphaël Amiard, Yannick Moy, Pierre-Marie de Rodat

Going After the Low Hanging Bug

At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).

#Static Analysis   

by Raphaël Amiard, Pierre-Marie de Rodat

Introducing Libadalang

AdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the only one. At AdaCore, we already have several other tools to process Ada code: the ASIS library, GNAT2XML, the GPS IDE. A realization of the past years, however, has been that we were lacking a unified solution to process code that is potentially evolving, potentially incorrect Ada code. Hence Libadalang.

#Ada    #tooling   

by Emmanuel Briot

Integrate new tools in GPS (2)

Customizing build target switches In the first post in this series (Integrate new tools in GPS) we saw how to create new build targets in GPS to spawn external tools via a menu or toolbar button, and then display the output of that tool in its own console, as well as show error messages in the Locations view.

#GPS   

by Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real Now?

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.

#Formal Verification    #SPARK   

by Emmanuel Briot

Integrate new tools in GPS

This blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small plugin might make your daily workflow more convenient by providing toolbar buttons and menus to spawn your tool and parse its output.

#GPS   

by Piotr Trojanek

Verifying Tasking in Extended, Relaxed Style

Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs allowed by the Ravenscar profile. Now it also supports the more relaxed GNAT Extended Ravenscar profile.

#Language    #Formal Verification    #SPARK   

by Emmanuel Briot

GNAT On macOS Sierra

GNAT and all the tools work great on the newly released macOS Sierra, but gdb needs some tweaking of the system.

#osx    #gdb   

by Emmanuel Briot

Debugger improvements in GPS 17

The GNAT Programming Studio support for the debugger has been enhanced. This post describes the various changes you can expect in this year's new release of GPS.

#GPS   

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.

#GitHub    #Ada    #GNAT    

by Emmanuel Briot

GNAT Programming Studio (GPS) on GitHub

The GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.

#GPS    #GitHub   

by Emmanuel Briot

Bookmarks in the GNAT Programming Studio (GPS)

As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view, and how you can now use it as a TODO list.

#GPS   

by Jérôme Lambourg

Efficient use of Simics for testing

As seen in the previous blog article, AdaCore relies heavily on virtualisation to perform the testing of its GNAT Pro products for VxWorks.

#Simics    #WindRiver    #GNAT Pro   

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.

#ARM    #emb2016    #embedded    #Embedded World   

by Fabien Chouteau

Make with Ada: Candy dispenser, with a twist...

A few months ago, my colleague Rebecca installed a candy dispenser in our kitchen here at AdaCore. I don’t remember how exactly, but I was challenged to make it more… fun.

by AdaCore Admin

Embedded Product Line Updates

Embedded products are not stand alone, this allows them to have safety, mission critical and real-time requirements that they wouldn’t necessarily have otherwise. The embedded product line provides analyzable, verifiable, and certifiable software for both static and dynamic analysis tools.

#AdaCoreTechDay    #GNAT     #Embedded Development    #embedded   

by Jérôme Lambourg

Porting the Ada Runtime to a new ARM board

A step by step tutorial to adapt the ARM runtime to new MCUs/boards.

#Bareboard    #ARM    #GNAT     #STM32    #Ravenscar   

by Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real?

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

#Formal Verification    #SPARK   

by Fabien Chouteau

Make with Ada: Formal proof on my wrist

When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.

#SPARK2014     #Smartwatch    #Makers   

by Emma Adby

Modernizing Adacore's Open-Source Involvement

Through the adoption of GitHub we have taken our first step on the way to having a more collaborative and dynamic interaction with, both our users and open source technologies.

#GitHub    #OSS    #Ada   

by AdaCore Admin

AdaCore Tech Days 2015

#AdaCoreTechDay    #GNAT Pro    #CodePeer    #SPARK Pro    #SPARK    #QGen   

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 Jack Mellor

2015: A Space Ada‑ssey

AdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed at the conference to see which ones!

#Space    #UK   

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?

#Makers    #NASA    #GtkAda    #Ada 2012   

by Cyrille Comar

Farewell Robert...

It is with great sadness that I have to announce the death of Robert Dewar...

#Robert Dewar   

by Yannick Moy

How Our Compiler Learnt From Our Analyzers

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.

#Compilation    #Formal Verification    #SPARK   

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 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.

#Storage Pools    #Ada    #memory management   

by Jamie Ayre

20 years on...

20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions

#20th Anniversary    #AdaLove   

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.

#GNAT Pro    #SPARK Pro    #GPS    #GNATbench    #GNATdashboard    #Ada    #AdaCore Factory    #CodePeer    #QGen   

by Yannick Moy

AdaCore Tech Days Prez on SPARK

Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.

by Yannick Moy

GNATprove Tips and Tricks: Catching Mistakes in Contracts

Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract. In this post, I show examples of incorrect constructs that are signaled by GNATprove.

#Formal Verification    #Compilation    #SPARK   

by Tristan Gingold

AdaCore at FOSDEM'15

I was at Bruxelles on January 31st to present the components of GNAT GPL 2015 : SPARK 2014 and GNAT GPL for ARM bare-board. This is not unrelated to a previous blog entry on Tetris in SPARK on ARM Cortex M4, in particular I presented that Tetris demo (I brought some boards with me and despite the simple package, none were broken!). The slides contain technical details on the ravenscar profile (main principles), how to build a program for the stm32f4-discovery board and how to port the runtime. There are also less technical slides such as why we choose the stm32f4 board and photos of some graphical demos. As that could be useful to anyone interested in Ravenscar or in porting the runtime to other boards or other platforms, we've made the slides available here.

#ARM    #Ravenscar    #FOSDEM    #GNATGPL   

by Yannick Moy

GNATprove Tips and Tricks: Keeping Justifications Up-To-Date

GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications may become obsolete across time. To help with that, GNATprove now issues a warning on useless justifications.

#Formal Verification    #SPARK   

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.

#SPARK    #ARM   

by Cyrille Comar

Welcome To AdaCore's Blog

I'm proud, if not a bit nervous, to be the one firing the very first post on this brand new blog. Why are we starting a corporate blog at this time? There are many reasons for this. The main one is that there are many things happening at AdaCore and around the GNAT technology and we are seeking better ways to make them widely known while offering interested recipients the possibility to react and interact with us.

by Yannick Moy

SPARK 2014 Rationale: Ghost Code

A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. If you're careful or lucky enough, the additional code you write will not impact the program being verified, and it will be removed during compilation, so that it does not inflate binary size or waste execution cycles. SPARK provides a way to get these benefits automatically, by marking the corresponding code as ghost code, using the new Ghost aspect.

#Formal Verification    #SPARK   

by Johannes Kanig

SPARK 15: Errors, Warnings and Checks

The messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the motivation behind it.

#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 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: 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   

by Yannick Moy

MISRA-C 2012 vs SPARK 2014, the Subset Matching Game

The MISRA C subset of C defines around 150 rules that restrict C programs for critical software development. Of these, 27 rules are classified as undecidable, which means that few MISRA C checkers (if any) will help checking those hardest rules. Here is how SPARK 2014 can help checking similar rules in Ada programs.

#Formal Verification    #SPARK    #MISRA-C   

by Yannick Moy

SPARK 2014 Rationale: Contract Cases

Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a contract by cases. A little history helps understanding how we came up with this new feature.

#Formal Verification    #SPARK