Week 7

Main topic of week 7: function correctness Definition

A function is being correct if when precondition holds, after executing the function, post condition follows. So, in order to prove a function is correct, we generally assume the precondition is true, and use induction to exam each step what happend there. Gerneralize all the result and compare it with the post condition. When proving it, we usually divide our proof into different cases, and form them we derive the postcondition.