Recitation 001

@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:

  1. assume precondition(1)
  2. show loop-invariant(2, 3) true

• PREServation: if we ever go into loop

  1. assume loop-invariant(2, 3), and loop_guard(5) true
  2. show loop-invariant(2', 3') remains true

• EXIT:

  1. assume loop-invariant(2, 3) is true, and loop_guard(5) false
  2. show correctness of the output

• TERMination:

  1. look at loop ("strictly decreasing towards, eventually")

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?)