Recitation 02

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 Tutorial.
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.