title: What is the loop invariance/invariant that can describe this code's functionality?
body: <pre><code>def func(no_1,no_2):
      a=no_1
      b=no_2
      while(b):
          a,b=b,a%b
      return a
  </code></pre>
  <p>where no_1 and no_2 are positive real numbers</p>
  <p>I've figured out that this function returns no_1 and no_2's greates common factor. First, I tried the loop invariance of (no_1%a and no_2%a) ≥ 0 such that a, no_1, and no_2 are positive integers but at termination, i can only prove that no_1%a = 0 = no_2%a, which does not describe the functionality at all. So can anyone tell me what possible loop invariance can this function have that describes its functionality?</p>