by
Fabien Chouteau
–
Ada for micro:bit Part 4: Pin Input
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
AdaCore Code of Conduct
Starting today, AdaCore has put in place a Code of Conduct (CoC) to ensure a positive environment for everyone willing and wanting to interact with us. With the development of this blog, our twitter accounts, and our GitHub corporate account, there is more and more communication between AdaCore and a number of communities. In this Code of Conduct we want to explain how we are going to moderate the AdaCore-maintained community spaces with the goal of maintaining a welcoming, friendly environment.
by
Fabien Chouteau
–
Ada for micro:bit Part 3: Pin Output
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by
Michael Frank
–
Code Obfuscator for Ada using Libadalang and SPARK
A code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This article shows an example of an Ada obfuscator, written in the SPARK language and using the Libadalang library to intelligently hide names and text within the source.
by
Fabien Chouteau
–
Ada for micro:bit Part 2: Push buttons
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by
Fabien Chouteau
–
Ada for micro:bit Part 1: Getting Started
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
GNATcoverage: getting started with instrumentation
This is the second post of a series about GNATcoverage and source code instrumentation. The previous post introduced how GNATcoverage worked originally and why we extended it to support source instrumentation-based code coverage computation. Let’s now see it in action in the most simple case: a basic program running on the host machine, i.e. the Linux/Windows machine that runs GNATcoverage itself.
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!
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: LoRaDa := Ada + LoRa;
Hedley Rainnie's project combines 6 different SoCs all programmed in Ada performing as a LoRa network. He also showcases a BLE bridge to a LoRa server. His project came about when him and his wife were musing about how to detect and deter unwanted garden visitors. This ongoing project won a finalist prize in the 2019/20 Make with Ada competition.
by
Claire Dross
–
Relaxing the Data Initialization Policy of SPARK
SPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like access types) or SPARK specific developments. However, new features generally take a while to make it into actual user code. The feature I am going to present here is in my experience an exception, as it was used both internally and by external users before it made it into any actual release. It was designed to enhance the verification of data initialization, whose limitations have been a long standing issue in SPARK.
by
Emma Adby
–
Make with Ada 2020: Disaster Management with Smart Circuit Breaker
Shahariar's project ensures safety against electrical fire or shock during an earthquake, flood, gas leakage or fire breakout by disconnecting the mains with a smart circuit breaker. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.
by
Emma Adby
–
Make with Ada 2020: CryptAda - (Nuclear) Crypto on Embedded Device
Team CryptAda's project collects entropy, manages an entropy pool, implements a homemade PRNG, and generates RSA keys directly on the board with an accent on security. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.
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.
CuBit: A General-Purpose Operating System in SPARK/Ada
Last year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only recently began work in high integrity software development and formal methods. There are several operating system projects, like the SeL4 microkernel and the Muen separation kernel, that make use of formal verification. But I was interested in using a formally-verified language to write a general-purpose OS - an environment for abstracting the underlying hardware while acting as an arbiter for running the normal applications we're used to.
by
Nicolas Setton
–
GNAT Community 2020 is here!
We are happy to announce that the GNAT Community 2020 release is now available! Read the post for access to download and to find out about this year's release highlights.
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
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
Johannes Kliemann
–
Ada on the ESP8266
Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to be the LLVM version of GNAT. This gave me to the idea to try out if LLVMs promise of providing modular and reusable toolchain technologies is true.
by
Martyn Pike
–
A Trivial File Transfer Protocol Server written in Ada
For an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user interaction. A protocol that's particularly appropriate for this kind of usage is the Trivial File Transfer Protocol (TFTP).