Inferred loop invariants
LOOP:
N = size(B)
S = sum(B[0..I-1])
¨
N in [7..13]
I in [0..13]
¨
I <= N
¨
B: All elements in [-100..100]
B[0..I-1]: All elements in [-100..100]
Skip this slide.
It’s here as a backup for questions if necessary.
Loop invariant: 0
i
n
and
s
= (
j
: 0
j
<
i
:
b
[
j
])
