Overview

Ada is an ISO-standardized programming language focusing on readability, correctness and reliability. Towards these goals it focuses on explicitness, strong typing, compile time and run time constraints on types, and minimum symbology.

Ada proves itself in reliability with a track record of nearly four decades of usage in embedded, safety, and critical systems. Over this timeframe, Ada was updated three times, each time with a new Reference Manual, a more in-depth Annotated Reference Manual, and a Rationale document, describing the reasoning for each feature. Backing each of these changes is the Ada Conformity Assessment Test Suite (ACATS), a battery of freely available tests to help Ada compilers or interprets properly interpret the standard. Ada 2012 takes reliability further, by supporting inline usage of an Ada subset called SPARK, which provides functional specification and static verification.

AdaCore provides GNAT Community edition, an all-in-one download for multiple platforms. This includes a cross-platform IDE with a code formatter, build system, documentation generator, integrated source control, auto-completion, and a visual diff tool. In addition to the Ada standard library, also included is the GNAT Components Collection (GNATColl) which includes facilities such as JSON parsing, the GNAT library (hashing, regex, sockets, etc.), Ada Web Server for communicating with browsers or providing services with your applications, libgpr for manipulating GNAT project files, aunit for unit testing, and libadalang for parsing and semantic analysis of Ada code. There’s also a Visual Studio Code Plugin or those who want to use their editor of choice can also use the Ada language server.

The emphasis on compile-time checks stops bugs at the earliest and cheapest point in development preventing them from being added to the program.

The focus on correctness extends static typing past “put the square peg in the square hole”. Ada prohibits implicit integer <-> float conversions, provides mechanisms to verify the range of values used for floating point and integer types, and compiler injection of invariant checks for user-defined types. Lightweight semantic variations of existing types can also be created which share the same underlying functions, but the compiler prevents mixing these types with different meanings unless explicit casts are used. This adds meaning to even low level types like integers and floating point values, preventing such mixing as accidentally adding a value meaning “joules” to one meaning “meters”.

Ada provides “access types”, allowing the creation of “typed pointers”, which integrates lifetime (“accessibility”) checks statically into the type system and providing separate customizable storage pools. “Anonymous” access types provide flexibility outside of this system without lifetime annotations by pushing lifetime checks to runtime.

Extensive runtime checks also help protect from memory safety errors (buffer overflows, accessing unallocated memory, invalid array access) as well as logical errors (range checks, pre/post condition checks, and type invariant checks). Though generally efficient and sometimes removable for checks which are known to never fail, runtime checks can also be suppressed in specific areas, such as performance critical areas, or throughout the program.

Ada supports built-in concurrency types for creating and synchronizing tasks to take advantage of today’s multiprocessor systems. Ada 2012 also incorporates the Ravenscar profile, a compiler pragma which restricts Ada to a subset for deterministic behavior of the system for real-time systems.

Ada’s history in high-reliability systems shows its focus on readability and correctness. As shown by its adoption by NVIDIA for security-critical firmware, Ada 2012 remains an attractive option for future software development.