Ada has a rich set of language features to express preconditions, postconditions, and invariants directly in the code, and then have those logical statements available to the compiler so that it can assume certain facts about the program's execution when optimizing:
Also, the type system lets you specify legal values with more precision than the word-based types that most languages inherited from C. For example, you can have range types that may hold integers of only a certain range, and the compiler will enforce that when assigning to variables of the type, or throw an exception if an arithmetic operation results in a value outside the range (you also have modulus types that explicitly give the wraparound behavior familiar in C). Containers allow generic constraints, and you can explicitly specify the dimensions of array types.
https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based...
Also, the type system lets you specify legal values with more precision than the word-based types that most languages inherited from C. For example, you can have range types that may hold integers of only a certain range, and the compiler will enforce that when assigning to variables of the type, or throw an exception if an arithmetic operation results in a value outside the range (you also have modulus types that explicitly give the wraparound behavior familiar in C). Containers allow generic constraints, and you can explicitly specify the dimensions of array types.
https://en.wikibooks.org/wiki/Ada_Programming/Type_System