PGCD impératif

let pgcd a b =
  let x = ref a and y = ref b in
  while !y <> 0 do
    let r = !x mod !y in
    x := !y;
    y := r
  done;
  !x

Variant : !y. Il reste positif tant que la condition !y <> 0 (avec !y initialement $\ge 0$) tient, et il décroît strictement car le nouveau !y vaut !x mod !y $<!y$. La boucle se termine donc.