A commercial proprietary  *(programming language) from _(EscherTech| http://www.eschertech.com/) 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| http://www.eschertech.com/support/perfect_developer_self_help.htm) section to see all the documentation and tutorials.

