Inductive loop invariant is a program assertion whose properties are sufficient to inductively prove that a code fragment satisfies the desired properties.

This is an informal definition of inductive loop invariant.

Given a procedure

proc p()
/*: requires Pre
    ensures Post */
{
  s1;
  while 
   (e) { 
   s2; 
  }
  s3;
}

we say I is an inductive loop invariant, written as

proc p()
/*: requires Pre
    ensures Post */
{
  s1;
  while /*: inv I */
   (e) { 
   s2; 
  }
  s3;
}

if the following three conditions hold:

1. I holds initially: in all states satisfying Pre, when execution reaches loop entry, I holds
2. I is preserved: if we assume that I and the loop condition (e) hold, then we can prove that I will hold again after executing s2
3. I is strong enough: if we assume that I holds and the loop condition (e) does not hold, then we can prove that Post holds after executing s3

Explanation: because I holds initially and it is preserved, by induction from holds initially and preserved follows that I will hold in every loop iteration. The strong enough condition ensures that when loop terminates, the rest of the program will satisfy the desired postcondition.