Finding loop invariant of Lowest common multiple function
Well, a possible loop invariant is "$x$ is a multiple of $a$ and $y$ is a multiple of $b$".

Then this almost proves partial correctness, because we know that after the loop terminates $\neg(x \neq y) \to x = y$, thus $x$ must be a multiple of both $a$ and $b$.

What this loop invariant doesn't show is that $x$ is the smallest possible such number.

To solve this, we must complicate our loop invariant:


If $x \geq y$, $x$ is the smallest multiple of $a$ that is bigger than or equal to $y$.
If $y \geq x$, $y$ is the smallest multiple of $b$ that is bigger than or equal to $x$.


Now it's up to you to prove that this invariant is correct.