# Notion of Inductive Loop Invariant

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:

*I***holds initially**: in all states satisfying*Pre*, when execution reaches loop entry,*I*holds*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**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.