Correctness

When we have a function, how can we show the function we write is correct?

Formally, we define the input and output, and try to prove input $\implies$ output

That is, after we have the definition of input and out, then we do following to prove a function's correctness:

1. define loop invariant
2. Initialization
3. Maintenance(inductive step)
4. Termination
5. Descending sequence

Actually, this part is the most tough part of the course where sometimes hard to find a intuitive way to prove correctness.