Eine Invariante ist eine Aussage, die über die Ausführung bestimmter Programmbefehle hinweg gilt. Sie ist also vor und nach diesen Befehlen wahr, sie ist demnach nicht veränderlich, also invariant. Invarianten können zum Beweis der Korrektheit von Algorithmen verwendet werden und spielen eine große Rolle im Design By Contract. Dabei werden für eine Methode einer Schnittstelle deren Vor- und Nachbedingungen und alle Invarianten in ihrem Ablauf beschrieben. Mittels sogenannter Assertions (Zusicherungen) kann man dieses Konzept implementieren, sofern es die verwendete Programmiersprache oder API unterstützt.
Siehe auch
Weblinks
- Programm zur automatischen Verifikation (auf der Seite ist auch eine auf Java portierte Version verlinkt)