The original design-by-contract language.

• Home page
• Tutorials
• AutoTest provides automatic test case extraction and test generation using the contracts themselves.
• AutoProof leverages SMT solvers to automatically prove if code satisfies a contract.

TODO List:

• Get through the entire tutorial.
• Get an understanding of the overall testing/verification infrastructure built on top of Eiffel’s design-by-contract approach.
  • Try out auto test.
  • Try out auto proof.