У рачунарским наукама, инваријанта представља логичку формулу за коју се сматра да је истинита за време извршавања програма, или неке његове фазе. На пример, инваријанта петље је логичка формула која укључује вредности променљивих које се јављају у петљи и која важи при сваком испитивању услова петље (непосредно пре, за време и непосредно након извршавања петље).
Инваријанта је нарочито корисна при разматрању коректности и верификацији рачунарских програма. Теорија оптимизације компајлера и формални методи за испитивање коректности програма су сви уско повезани са инваријантом. Програмери често употребљавају тврдње да би у свом коду инваријанту експлицитно навели. Неки објектно оријентисани програмски језици имају посебну синтаксу за означавање инваријаната класа.
MУ слагалица (енг. MU puzzle) је добар пример логичког проблема где је одлучивање преко инваријанте корисно. Игра почиње тако што се креће од речи МИ коју треба трансформисати у реч МУ, користећи у сваком кораку једно од следећих правила трансформације:
Пример (бројеви на стрелицама означавају које правило је примењено):
Да ли је могуће превести ниску МИ у ниску МУ користећи само четири наведена правила?
Могло би се провести доста сати примењивајући ова правила трансформације на ниску. Међутим, можда би било брже пронаћи предикат који је инваријантан на сва правила, и чини МУ нерешивим. Логички гледано, једини начин да се карактер И избаци из ниске је постојање три узастопна карактера И у ниски. Имајући ово на уму, размотримо следећу инваријанту:
Ово је инваријанта за проблем ако за сваку од трансформација важи следеће: Ако инваријанта важи пре примењивања правила, онда ће важити после примењивања правила такође. Ако обратимо пажњу на крајњи продукт примењивања правила на број карактера И и У можемо закључити да је ово случај за сва правила:
Правило | #И | #У | Ефекат на инваријанту |
---|---|---|---|
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
}