@requires: precondition @ensures: postconditions @loop_invariant: before loop guard
Exit: show correctness Termination: show loop terminates
precondition: 1
loop-invariant: 2, 3
assert: 4
postconditions: after 4 (usually checking for result)
proving:
INITialization:
PREServation: if we ever go into loop
EXIT:
TERMination:
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