XGCD
The Unit notes and lecture notes showed the Extended Euclidean
GCD Algorithm as a recursive algorithm. Here's an iterative
version:
Algorithm: XGCD(x,y)
Input : integers x,y ≥ 0
Output: g,s,t such that g is the gcd of x and y, and g = s*a + t*b

(a,b) = (x,y)
(sa,ta) = (1,0)
(sb,tb) = (0,1)
while b != 0 do
(q,r) = divide(a,b) ← i.e. a = q*b + r, 0 ≤ 0 < b
sbp = sa  q*sb
tbp = ta  q*tb
(sa,ta) = (sb,tb)
(sb,tb) = (sbp,tbp)
(a,b) = (b,r)
return (a, sa, ta);
}
Great, huh? But do you actually have any reason to believe it
works? What would it take to convince you that it works? This
is actually quite a simple algorithm in the grand scheme of
things, but already it's hard to be confident it is correct.
Let me try to convince you! Here's a loop invariant for you:
\[
a = s_a x + t_a y \text{ and } b = s_b x + t_b y
\]
So let's do this:

Initialization: As we encounter the loop for the
first time, we have
\[
a = x = 1\cdot x + 0\cdot y = s_a x + t_a y \text{ ... check!}
\text{ and we have }
b = y = 0\cdot x + 1\cdot y = s_b x + t_b y \text{ ... check!}
\]
So the invariant holds at the beginning

Matainance:
Assuming the invariant holds, we have
\[
a = qb + r \Rightarrow
r = a  qb = (s_a x + t_a y)  q(s_b x + t_b y)
= (s_a  q s_b) x + (t_a  q t_b) y = s'_b x + t'_b y
\]
Then we set $(s_a,t_a) = (s_b,t_b)$ so that after the
assignment $a = b$ we have the first part of the invariant.
Then we set $(s_b,t_b) = (s'_b,t'_b)$ so that after the
assignment $b = r$ we have the second part of the invariant.

Termination:
When the loop exits, $a$ is the gcd of $x$ and $y$, as
required. The loop invariant tells us that $a = s_a x + t_a
y$, so returning $(g,s,t) = (a,s_a,t_a)$ meets the
algorithm's specification.
Some important notes: The loop invariant
is not the
loop continuation condition. It is something new that is not in
the code, but tells us something extra about the code. Second,
the loop invariant references variables from the program,
referring to their value
at a point in time. We don't
write something like "$a_i$", intending to indicate the value of
$a$ "at the $i$th iteration". That's not how it works. The
invariant is true each and every time we get to the point where
we are about to check the loop continuation condition.
Finally, the invariant is strong enough that, we can easily use
it to prove the program correct.