Correctness of an algorithm difference between recursive and iteraive I know that the general strategy to do the correction of an algorithm is as follow : 


  
  if the algorithm is recursive then prove the correctness using induction
  if the algorithm is iterative (using a for loop for example) then find an invariant
  


Finding an invariant is sometimes hard while induction is easy. So since every iterative algorithm can be transformed into a recursive one, why do we bother finding clever invariant while we could do : 


  find the recursive equivalent algorithm -> use induction


Maybe the part : "transform the iterative program into a recursive one" is hard, but for simple programs it's definitely worth it. I mean sometimes it is (at least for me) very hard to find invariant, but when doing induction everything is "easy". 

So I guess I am missunderstanding something ?

Thank you !
A proof using a loop invariant is also a proof by induction – you prove that the invariant is indeed an invariant by induction. The reason that finding the inductive hypothesis is easier for recursive procedures is that we usually state the semantics of the recursive function – what it is supposed to compute – and this is the "loop invariant" we use to prove its correctness.

Let's consider the following two procedures for summing an array $A[1],\ldots,A[n]$:


  Iterative:
  
  
  $sum \gets 0$
  $i \gets 1$
  While $i \leq n$:
  
  
  $sum \gets sum + A[i]$
  $i \gets i + 1$
  
  Return $sum$
  
  
  Recursive:
  
  $Sum(A[1],\ldots,A[n])$
  
  
  If $n = 0$, Return $0$
  If $n &gt; 0$, Return $Sum(A[1],\ldots,A[n-1]) + A[n]$
  


The loop invariant for the iterative algorithm is $sum = A[1] + \cdots + A[i-1]$. This is something we have to come up with. We prove that it holds by induction, and conclude that the function returns $A[1] + \cdots + A[n]$.

In contrast, it is clear what $Sum$ is supposed to compute: the sum of its input. We still need to argue inductively that $Sum$ works correctly, but the inductive hypothesis $$Sum(A[1],\ldots,A[i]) = A[1] + \cdots + A[i]$$ corresponds to the semantics of $Sum$.

We often attach a meaning to recursive procedures, but not so often to loops. If we did attach a semantic meaning to the $i$'th iteration, it would become easy to formulate the loop invariant. An example is the Floyd–Warshall algorithm (or rather, some of its implementations), where the $i$'th iteration computes the shortest path of length at most $i$.