Eiffel
Eiffel is an object-oriented language based on
Ada designed by Betrand Meyer.
It provides formal support for pre-conditions by allowing
a programmer to insert assert statements at
appropriate points in his code.
Reference
Bertrand Meyer, "Eiffel: The Language", Prentice Hall, 1992
ISBN 0-13-247925-7.
There is also an
Eiffel Home Page.