Loop Invariants — arrayMax
Array
A
:
Apply
Presets:
5 2 9 3 9 7
increasing
max first
n = 1
random
⏮ First
← Prev
Next →
⏭ Last
▶ Play
Speed
arrayMax
We have to prove
𝐼 holds at (A)
𝐼 ∧ cond at (B) ⇒ 𝐼 at (C)
𝐼 ∧ ¬cond ⇒ post condition
Loop invariant
𝐼 ≡ curMax = max
k∈[0..
j
−1]
A
[k] ∧
j
≤
n
comparisons
A
[
j
] > curMax:
0
of
0
updates of curMax:
0
total work:
Θ(n)
← / → step · Home / End jump to start / end · Space plays