A commercial proprietary programming language from EscherTech that involves programming by contract. It looks a bit like Java, but actually you don't write any executable code: you just specify preconditions, postconditions and assertions, and hope that the compiler can fill in all the gaps and prove the correctness of all your assertions.

Go to the Self Help section to see all the documentation and tutorials.

This page is linked from: Design by Contract