Contracts enable specifying conditions that must hold true when the flow of runtime execution reaches the contract. If a contract is not true, then the program is assumed to have entered an undefined state.