Loop Invariant ?

En loop invariant beskriver kriterierne for, hvornår et loop er sandt. Dvs. under hvilke betingelser skal det respektive loop udføres og stoppe igen.

// { 0 <= i = N }
for (int i = 0; i < N; i++)
{
// do something
}

Invariant notationen er måske ikke helt korrekt men har lidt problemer med at skrive de matematiske symboler herinde.

Der findes preprocessorer, der kan tage disse invariant notationer og sørge for automatisk at generere kode udfra dem, så det bliver kontrolleret at invarianterne er overholdt. Et eksempel på dette er IContract (Java), denne har dog ikke loop invarianter, men metode- og klasse invarianter.

Hth