Invarijanta (računarstvo)

U računarskim naukama, invarijanta predstavlja logičku formulu za koju se smatra da je istinita za vreme izvršavanja programa, ili neke njegove faze. Na primer, invarijanta petlje je logička formula koja uključuje vrednosti promenljivih koje se javljaju u petlji i koja važi pri svakom ispitivanju uslova petlje (neposredno pre, za vreme i neposredno nakon izvršavanja petlje).

Upotreba

Invarijanta je naročito korisna pri razmatranju korektnosti i verifikaciji računarskih programa. Teorija optimizacije kompajlera i formalni metodi za ispitivanje korektnosti programa su svi usko povezani sa invarijantom. Programeri često upotrebljavaju tvrdnje da bi u svom kodu invarijantu eksplicitno naveli. Neki objektno orijentisani programski jezici imaju posebnu sintaksu za označavanje invarijanata klasa.

Primer

MU slagalica (eng. MU puzzle) je dobar primer logičkog problema gde je odlučivanje preko invarijante korisno. Igra počinje tako što se kreće od reči MI koju treba transformisati u reč MU, koristeći u svakom koraku jedno od sledećih pravila transformacije:

Ako se niska završava na karakter I, karakter U može biti nadovezan (xI -> xIU)
Niska koja se nalazi posle karaktera M može biti kompletno duplirana (Mx -> Mxx)
Bilo koja tri uzastopna karaktera I (III) mogu biti zamenjena jednim karakterom U (xIIIy -> xUy)
Bilo koja dva uzastopna karaktera U mogu biti izbrisani (xUUy -> xy)

Primer (brojevi na strelicama označavaju koje pravilo je primenjeno):

MI →² MII →² MIIII →³ MUI →² MUIUI →¹ MUIUIU →² MUIUIUUIUIU →⁴ MUIUIIUIU → ...

Da li je moguće prevesti nisku MI u nisku MU koristeći samo četiri navedena pravila?

Moglo bi se provesti dosta sati primenjivajući ova pravila transformacije na nisku. Međutim, možda bi bilo brže pronaći predikat koji je invarijantan na sva pravila, i čini MU nerešivim. Logički gledano, jedini način da se karakter I izbaci iz niske je postojanje tri uzastopna karaktera I u niski. Imajući ovo na umu, razmotrimo sledeću invarijantu:

Broj karaktera I u niski nije umnožak broja 3.

Ovo je invarijanta za problem ako za svaku od transformacija važi sledeće: Ako invarijanta važi pre primenjivanja pravila, onda će važiti posle primenjivanja pravila takođe. Ako obratimo pažnju na krajnji produkt primenjivanja pravila na broj karaktera I i U možemo zaključiti da je ovo slučaj za sva pravila:

Pravilo	#I	#U	Efekat na invarijantu
1	+0	+1	Broj karaktera I je nepromenjen. Ako je invarijanta važila, i dalje važi.
2	×2	×2	Ako n nije umnožak broja 3, onda 2xn nije takođe. Invarijanta i dalje važi.
3	−3	+1	Ako n nije umnožak broja 3, n-3 nije takođe. Invarijanta i dalje važi.
4	+0	−2	Broj karaktera I je nepromenjen. Ako je invarijanta važila, i dalje važi.

Tabela iznad jasno prikazuje da je invarijanta održiva za svako moguće pravilo transformacije, što u stvari znači da koje god pravilo uzmemo, u bilo kom stanju, ako broj karaktera I nije umnožak broja 3 pre primenjivanja pravila, neće biti ni posle primenjivanja.

Zaključujemo da postoji jedan karakter I u niski MI, a broj 1 nije umnožak broja 3, pa iz toga sledi da je nemoguće transformisati nisku MI u nisku MU jer 0 nije umnožak od 3.

Automatska detekcija invarijante u imperativnom programiranju

Alati za apstraktnu interpretaciju mogu izračunati jednostavne invarijante imperativnih programa. Vrsta svojstva koja može biti pronađena zavisi od apstraktnog domena koji se koristi. Tipični primeri svojstva su celobrojne promenljive opsega 0<=x<1024, veza između nekoliko promenljivih kao 0<=i-j<2*n-1, ili informacije kao y%4==0.^[1]

Sofisticiranije invarijante moraju biti ručno predstavljene. Praktično, verifikovanje imperativnih programa korišćenjem Horove logike, invarijante petlje moraju biti ručno predstavljene za svaku petlju u programu, što je jedan od razloga zbog čega je taj zadatak veoma naporan.^[2]

U primeru ispod, ni jedan alat ne bi bio u mogućnosti da detektuje, iz pravila 1-4, da je MU slagalica nemoguća. Medjutim, ako bi MU slagalica bila opisana sledećim S kodom, alati za apstraktnu interpretaciju bi mogli da detektuju da ICount%3 ne može biti 0 i da se nikada neće iskočiti iz "while" petlje.

void MUPuzzle(void) {
    volatile int RandomRule;
    int ICount=1, UCount=0;
    while (ICount%3!=0)                            // non-terminating loop
        switch(RandomRule) {
        case 1:                UCount+=1;   break;
        case 2:   ICount*=2;   UCount*=2;   break;
        case 3:   ICount-=3;   UCount+=1;   break;
        case 4:                UCount-=2;   break;
        }                                          // computed invariant: ICount%3==1||ICount%3==2
}

Reference

^ Bouajjani, A.; Drǎgoi, C.; Enea, C.; Rezine, A.; Sighireanu, M. (2010). „Invariant Synthesis for Programs Manipulating Lists with Unbounded Data”. Proc. CAV.
^ Hoare, C. A. R. (1969). „An axiomatic basis for computer programming”. Communications of the ACM. 12 (10): 576—580. S2CID 207726175. doi:10.1145/363235.363259.

Spoljašnje veze

Applet: Visual Invariants in Sorting Algorithms Arhivirano na sajtu Wayback Machine (24. februar 2022)

[1] Bouajjani, A.; Drǎgoi, C.; Enea, C.; Rezine, A.; Sighireanu, M. (2010). „Invariant Synthesis for Programs Manipulating Lists with Unbounded Data”. Proc. CAV.

[2] Hoare, C. A. R. (1969). „An axiomatic basis for computer programming”. Communications of the ACM. 12 (10): 576—580. S2CID 207726175. doi:10.1145/363235.363259.

[1]

[2]