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)
Rationale for the Design of the ADA Programming Language.pdf
(Jean D. Ichbiah,
John G. P. Barnes,
Jean-Claude Heliard,
Bernd Krieg-Brueckner,
Olivier Roubine,
Brian A. Wichmann
1979)