. Preconditions and postconditions define the expectations and obligations of a subprogram.
. Type invariants specify boundary constraints for objects of an encapsulated (private) type.
. Subtype predicates capture general constraints on data objects.
. Expression functions offer a convenient way to express simple functions.
. Conditional expressions provide a compact notation for a common idiom.
. Quantified expressions for universal and existential forms specify predicates over arrays and containers.
Concurrency and Multicore Support
. Task affinities and dispatching domains allow tasks to be mapped to specific CPUs or cores.
. Ravenscar for multiprocessor systems adapts a safe and widely used tasking profile to modern architectures.
. Bounded containers use stack allocation and do not incur the overhead of dynamic memory management.
.Task-safe queues and priority queues provide efficient implementations of synchronized structures.
.Holder containers create singleton structures for objects of an unconstrained type.
. Iterators provide familiar idioms with uniform syntax to search and manipulate arrays and containers.
See relating links:
High-integrity object-oriented programming with Ada
High-integrity object-oriented programming with Ada - Part 1
High-integrity object-oriented programming with Ada – Part 2
High-integrity object-oriented programming with Ada - Part 3
Developing secure code using SPARK (Part 1)
Developing secure code using SPARK (Part 2)
If you found this article to be of interest, visit Military/Aerospace Designline
where you will find the latest and greatest design, technology,
product, and news articles with regard to all aspects of military,
defense and aerospace. And, to register to our weekly newsletter, click here.