title: What's the loop invariant for this code?
body: <p>I need to come up with a loop invariant for a given piece of code:</p>
  
  <pre><code>//pre: x &amp; y &gt;= 0
  //post: z = x^y
  //computes pow(x, y), x^y
  int pow(int x, int y){
      int z = 1;
      while(y &gt; 0){
          if(y%2==0){
              y /= 2;
              x = x*x;
          }else{
              z = z*x;
              y -= 1;
          }
      }
      return z;
  }
  </code></pre>
  
  <p>My invariant is:</p>
  
  <pre><code>{(ypre - 0 = 0 &amp; x = x^(ypre  -y)) OR (ypre - y != 0 &amp; x^(n + m) = x^(ypre - y), where (n=ypre-y) and (m=integer value of z/x))}
  </code></pre>
  
  <p>This is a messy invariant, and I'm not 100% sure it's correct. Is there a better invariant that would cover the post condition of z = x^y</p>