For the record: that was ages ago, the language has improved a lot since then. Ada 2012 includes features for contracts, for example. Read the "Preface" of "Programming in Ada 2012" for details. :)
The Ariane 5 failure was due to the faster trajectory of that launcher causing an integer overflow that the Ariane 4 (which the software was cribbed from) did not experience. I'm not clear how you encode that in a contract.
The sad thing about this is that if that code had been in (say) C the launch would have been fine, since no integer overflow would have been trapped, shutting down the guidance computer.
