Инваријанта (рачунарство)

У рачунарским наукама, инваријанта представља логичку формулу за коју се сматра да је истинита за време извршавања програма, или неке његове фазе. На пример, инваријанта петље је логичка формула која укључује вредности променљивих које се јављају у петљи и која важи при сваком испитивању услова петље (непосредно пре, за време и непосредно након извршавања петље).

Употреба

Инваријанта је нарочито корисна при разматрању коректности и верификацији рачунарских програма. Теорија оптимизације компајлера и формални методи за испитивање коректности програма су сви уско повезани са инваријантом. Програмери често употребљавају тврдње да би у свом коду инваријанту експлицитно навели. Неки објектно оријентисани програмски језици имају посебну синтаксу за означавање инваријаната класа.

Пример

MУ слагалица (енг. MU puzzle) је добар пример логичког проблема где је одлучивање преко инваријанте корисно. Игра почиње тако што се креће од речи МИ коју треба трансформисати у реч МУ, користећи у сваком кораку једно од следећих правила трансформације:

Ако се ниска завршава на карактер И, карактер У може бити надовезан (xИ -> xИУ)
Ниска која се налази после карактера М може бити комплетно дуплирана (Мx -> Мxx)
Било која три узастопна карактера И (ИИИ) могу бити замењена једним карактером У (xИИИy -> xУy)
Било која два узастопна карактера У могу бити избрисани (xУУy -> xy)

Пример (бројеви на стрелицама означавају које правило је примењено):

MИ →² MИИ →² MИИИИ →³ MУИ →² MУИУИ →¹ MУИУИУ →² MУИУИУУИУИУ →⁴ MУИУИИУИУ → ...

Да ли је могуће превести ниску МИ у ниску МУ користећи само четири наведена правила?

Могло би се провести доста сати примењивајући ова правила трансформације на ниску. Међутим, можда би било брже пронаћи предикат који је инваријантан на сва правила, и чини МУ нерешивим. Логички гледано, једини начин да се карактер И избаци из ниске је постојање три узастопна карактера И у ниски. Имајући ово на уму, размотримо следећу инваријанту:

Број карактера И у ниски није умножак броја 3.

Ово је инваријанта за проблем ако за сваку од трансформација важи следеће: Ако инваријанта важи пре примењивања правила, онда ће важити после примењивања правила такође. Ако обратимо пажњу на крајњи продукт примењивања правила на број карактера И и У можемо закључити да је ово случај за сва правила:

Правило	#И	#У	Ефекат на инваријанту
1	+0	+1	Број карактера И је непромењен. Ако је инваријанта важила, и даље важи.
2	×2	×2	Ако n није умножак броја 3, онда 2xn није такође. Инваријанта и даље важи.
3	−3	+1	Ако n није умножак броја 3, n-3 није такође. Инваријанта и даље важи.
4	+0	−2	Број карактера И је непромењен. Ако је инваријанта важила, и даље важи.

Табела изнад јасно приказује да је инваријанта одржива за свако могуће правило трансформације, што у ствари значи да које год правило узмемо, у било ком стању, ако број карактера И није умножак броја 3 пре примењивања правила, неће бити ни после примењивања.

Закључујемо да постоји један карактер И у ниски МИ, а број 1 није умножак броја 3, па из тога следи да је немогуће трансформисати ниску МИ у ниску МУ јер 0 није умножак од 3.

Аутоматска детекција инваријанте у императивном програмирању

Алати за апстрактну интерпретацију могу израчунати једноставне инваријанте императивних програма. Врста својства која може бити пронађена зависи од апстрактног домена који се користи. Типични примери својства су целобројне променљиве опсега 0<=x<1024, веза између неколико променљивих као 0<=i-j<2*n-1, или информације као y%4==0.^[1]

Софистицираније инваријанте морају бити ручно представљене. Практично, верификовање императивних програма коришћењем Хорове логике, инваријанте петље морају бити ручно представљене за сваку петљу у програму, што је један од разлога због чега је тај задатак веома напоран.^[2]

У примеру испод, ни један алат не би био у могућности да детектује, из правила 1-4, да је МУ слагалица немогућа. Медјутим, ако би МУ слагалица била описана следећим С кодом, алати за апстрактну интерпретацију би могли да детектују да ICount%3 не може бити 0 и да се никада неће искочити из "while" петље.

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
}

Референце

^ 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.

Спољашње везе

Applet: Visual Invariants in Sorting Algorithms Архивирано на сајту Wayback Machine (24. фебруар 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]