[Ada] Ada / SPARK

Ada

Ada is a structured, statically typed, imperative, and object-oriented high-level programming language, extended from Pascal and other languages. It has built-in language support for design by contract (DbC), extremely strong typing, explicit concurrency, tasks, synchronous message passing, protected objects, and non-determinism. Ada improves code safety and maintainability by using the compiler to find errors in favor of runtime errors. (presentation on Wikipedia)

SPARK

The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification. (presentation on Wikipedia)

[Ada] Ada implementations

Documentations

Libraries

Tools

Verification

Ada history

Miscellaneous