[elviejo]

Eiffel is the language you are looking for. It's pre-conditions and post-conditions prove the properties of the code that you actually are executing.

The book that does the equivalent but with the properties checked at runtime is: Object Structures (like data structures but with objects).

Here is the link:

https://openlibrary.org/works/OL2979696W/Object_structures?e...