Invariant (informatica)

In de informatica is een invariant een predicaat dat dezelfde waarheidswaarde behoudt tijdens het uitvoeren van een stuk code.

Het bepalen van invarianten van (gedeelten van) broncode wordt veel gedaan wanneer men wil redeneren over de werking en de correctheid van een computerprogramma. Invarianten worden veel gebruikt bij compileroptimalisatie, Design by Contract en formele methoden voor het bepalen van de correctheid van een computerprogramma.

Programmeurs maken vaak gebruik van asserties om de invarianten expliciet te vermelden.

Klasse-invariant

In objectgeoriënteerde programmeertalen bestaan ook klasse-invarianten die de toestanden die een object van een klasse kan aannemen vastleggen. De methoden van de klasse dienen deze invarianten in stand te houden. Een klasse-invariant wordt vaak bij het construeren van het object vastgelegd en deze wordt behouden wanneer er publieke methoden worden uitgevoerd. Het is mogelijk de klasse-invariant tijdelijk te schenden tussen aanroepen van interne (private) methoden maar dit is niet aan te raden aangezien het object zich dan tijdelijk in een ongeldige toestand bevindt.

De klasse-invariant legt vast welke waarden de velden van het object kan aannemen en daarmee ook welke toestanden (mogelijke waarden van de velden) geldig zijn en welke niet. Net zoals een invariant kan een klasse-invariant helpen bij het redeneren over de werking van een objectgeoriënteerd programma en welke aannamen programmeurs mogen maken wanneer ze een object van een klasse gebruiken. Een klasse-invariant moet gelden na afloop van de constructor en voor en na het aanroepen van een publieke methode.

De meeste objectgeoriënteerde programmeertalen ondersteunen asserties waarmee klasse-invarianten genoteerd kunnen worden. In sommige talen is er ook een aparte syntaxis om een klasse-invariant te noteren. Java heeft bijvoorbeeld de Java Modeling Language waarmee dergelijke invarianten genoteerd kunnen worden.

Voorbeeld

Het volgende is een voorbeeld van klasse-invarianten in Java met de notatie van de Java Modeling Language; deze definieert een syntaxis voor de annotations die in Java bij methoden geplaatst kunnen worden. Publieke methoden dienen een preconditie en een postconditie op te geven om de klasse-invariant in stand te houden.

public class Date
{
    int /*@spec_public@*/ day;
    int /*@spec_public@*/ hour;
    
    /*@invariant 1<=day && day <=31; @*/     // klasse-invariant
    /*@invariant 0<=hour && hour < 24; @*/   // klasse-invariant
    
    /*@ 
      @requires 1 <= d && d <=31; 
      @requires 0<=h && h < 24; 
      @*/
    public Date(int d, int h){ day = d; hour = h; } // constructor
    
    /*@ 
      @requires 1 <= d && d <=31; 
      @ensures day == d;
      @*/
    public void setDay(int d) 
    {
        if(1 <= d && d <=31)
            day = d;
    }
   
    /*@ 
      @requires 0<=h && h < 24;
      @ensures hour == h;
      @*/
    public void setHour(int h)
    {
         if(0<=h && h < 24)
           hour = h;
    }

}