We have the following i <- 0 j <- 0 x <- 1 y <- 1 z <- 1 c <- 1 u <- 1 while i<n do    i <- i+1    j <- i    x <- x*i    z <- x    y <- i+1    y <- x*y    while j<2*i do       j <- j+1       z <- z*j    od    c <- z div (x*y) od I want to find the loop invariant for both while-loops. I applied the algorithm some times to understand what it does: The inner while loop calculates the following: $$z=z\prod_{m=1}^{2i-1}(i+m)=x\prod_{m=1}^{2i-1}(i+m)$$ or not? Is this also the loop invariant of the inner while loop? So I got the following results: First loop: i=1 j=i=1 x=1 z=x=1 y=i+1=2 y=x*y=2 inner while loop: z=x(i+1)=2 c = z div (x*y) = 2 div 2 = 1 Second loop: i=2 j=i=2 x=1*2=2 z=x=2 y=i+1=3 y=x*y=2*3=6 inner while loop: z=x(i+1)(i+2)(i+3)=2*3*4*5 c = z div (x*y) = 2*3*4*5/2*6=10 Third loop: i=3 j=i=3 x=2*3=6 z=x=6y=i+1=4 y=x*y=24 inner while loop: z=x(i+1)(i+2)(i+3)(i+4)(i+5)=6*4*5*6*7*8 c = z div (x*y) = 6*4*5*6*7*8/6*24=5*7*8=280Is everything correct? But what exactly calculates the algorithm? What is a general formula of the results?  
What does the algorithm calculate?
algorithms;correctness proof;loop invariants
Note that $x=i!$. Now it's easy to see $y=(i+1)!$ and $z=(2i)!$. So $c=\frac{(2i)!}{i!(i+1)!}$, which is the $i$th Catalan number.P.S. Your formula is wrong. The condition of the inner loop is $j=i+m\le2i$, so $m$ is from $1$ to $i$ instead of $2i-1$ or something.