Invariante (Informatik)

Eine Invariante ist eine Bedingung, die in jedem Programmzustand erfüllt sein muss. Bei der Implementierung einer Schleife muss beispielsweise innerhalb dieser immer gelten, dass die Schleifenvariable kleiner ist als der Wert der Abbruchbedingung.

Beispiel:

FOR a = 1 TO 5 NEXT 1 (Zähle a von 1 nach 5 in Einerschritten hoch)

PRINT a (Gebe a auf dem Bildschirm aus)

NEXT a (Wiederhole die Schleife, es sei denn a ist bereits 5)

END (Beendet das Programm)

In diesem Beispiel ist die Invariante a<5 als Bedingung für die Wiederholung der Schleife.

Invarianten können zum Beweis der Korrektheit von Algorithmen verwendet werden.

Invarianten spielen eine große Rolle im Contract Based Design. Dabei werden für eine Methode einer Schnittstelle, deren Vor- und Nachbedingungen und alle Invarianten in ihrem Ablauf beschrieben.