• What does the function pxe defined below do?
• Prove (by loop invariant, of course) that the function does correctly what you think it does.
• What is the time complexity of pxe as a function of a and b?

function pxe(a,b: integer): integer;
begin x,y,z:=a,b,1;
      while y > 0 do
      begin while even(y) do x,y:=x²,y/2;
            y,z:=y-1,x*z
            end;
      pxe:=z
      end;