Recitation 02: Contracts
- Discussed the types of contracts used in C0, what each is used for,
and resoning through code. For discussion on what each is used for, how to
write effective contracts, and the syntax involved, refer to the C0
- Good contracts should be strong enough that they allow you to show
that the function is correct. Preconditions allow us to make assumptions
about the input values and postconditions are used to check that the
returned value obeys the function specification. Assertions and loop
invariants are used to bridge the gap between the pre/post conditions to
show that, if the preconditions are met, the result must be correct.
- Avoid uninformative or redundant contracts. If I have a function of
type bool, //@ensures \result == true || \result ==
false is not a useful statement. If and only if a function can
operate on any input value, it is okay to not state a precondition.
- Be careful about when loop invariants are tested. They must be true
right before the exit condition is tested. This means that it must hold
before entering the loop body the first time, at the end of each
iteration, and at the end of the final iteration. This means that even if
the loop body is never entered, the invariant still must hold. These
factors play an essential role in proving correctness.
- Carefully written contracts will make debugging an easier process.
- The examples using the pow() function can be found here.
If you have any comments or see any errors, please
let me know.