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; 
  }
}

we say I is an inductive loop invariant, written as

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

if the following conditions hold:

1. I holds initially: in all states satisfying Pre, when execution reaches loop entry,