Recitation 001

@requires: precondition @ensures: postconditions @loop_invariant: before loop guard

Exit: show correctness Termination: show loop terminates


TODO 5?? Alex Lin TODO why is not 4 post condition (what ensures do) => when is ensure checked? (if it checks at the same place as @assert, then... why not)

-> exit(correct, ) -> termination(is going to end?)

Table of Content