Abstraktne interpretatsioon

Abstraktne interpretatsioon (inglise keeles abstract interpretation) on informaatika teooria arvutiprogrammide semantika korrektseks lähendamiseks, põhinedes monotoonsetel funktsioonidel üle osaliselt järjestatud hulkade, eelkõige võrede. Seda võib vaadelda kui arvutiprogrammi osalist täitmist, millega kogutakse informatsiooni selle semantika (nt juhtimisvoo, andmevoo) kohta, tegemata kõiki arvutusi.

Selle teooria põhiline rakendus on formaalne staatiline analüüs, mis hangib informatsiooni programmide võimalike täitmiste kohta. Sellistel analüüsidel on kaks põhilist kasutusvaldkonda:

• kompilaatorites, et analüüsida programme, otsustamaks, kas mingid automaatsed optimeerimised on võimalikud;
• silumisel, et leida programmidest vigu neid käivitamata.

Abstraktse interpretatsiooni teooria formaliseerisid prantsuse informaatikud Patrick Cousot ja Radhia Cousot 1970. aastate lõpus. Esimene suuremahuline automaatne programmianalüüs abstraktse interpretatsiooni abil teostati Ariane 5 raketi koodil pärast selle esmalennu ebaõnnestumist 1996. aastal.

Abstraktsed domeenid

Abstraktseks interpretatsiooniks kasutatavaid võresid nimetatakse abstraktseteks domeenideks (inglise keeles abstract domain). Domeeni elemendid on programmi konkreetsete seisundite lähendused, millel sooritatakse konkreetsetele operatsioonidele vastavaid abstraktseid operatsioone. Lähendamine ja sellega kaasnev täpsuse kaotus võib olla vajalik, et semantika oleks lahenduv (vt Rice'i teoreem, peatumisprobleem).

Domeeni valik sõltub sellest, milliste programmi omaduste kohta informatsiooni otsitakse. Lisaks tuleb teha kompromiss selle täpsuse ja keerukuse vahel.

Täisarvude domeenid

Täisarvuliste muutujate ja nende tehete lähendamiseks on abstraktsel interpreteerimisel mitmeid võimalusi.

Kombinatsioon intervallaritmeetikast (roheline) ja kongurentsist mod 2 (sinine) abstraktsete domeenidena, et analüüsida C programmi (punane: konkreetsed võimalike väärtuste hulgad täitmisel). Kasutades jääke (0=paaris, 1=paaritu), saab nulliga jagamise välistada

Märkide domeen

Selliste muutujate puhul võib unustada täpsed väärtused, jättes alles ainult nende väärtuste märgid (+, - või 0). Mõningate aritmeetiliste tehete, näiteks korrutamise puhul selline lähendus täpsust ei kaota: kahe täisarvu korrutise märk on üheselt määratud korrutatud arvude märkidega. Teiste tehete, näiteks liitmise puhul lähendus võib kaotada täpsust: positiivse ja negatiivse arvu summa märki pole võimalik ainult liidetavate märke teades määrata.

Intervallide domeen

Täpsemaks analüüsiks võib kasutada näiteks arvtelje lõike, kirjeldades iga muutuja $x$ võimalikke väärtusi täisarvude intervalliga $[l_{x},u_{x}]$. Sellistel lähendustel on võimalik defineerida aritmeetilised tehted, moodustades intervallaritmeetika. Näiteks muutujate $x$ ja $y$, mille intervallid on vastavalt $[l_{x},u_{x}]$ ja $[l_{y},u_{y}]$, korral on

• summa $x+y$ intervall $[l_{x}+l_{y},u_{x}+u_{y}]$,
• vahe $x-y$ intervall $[l_{x}-u_{y},u_{x}-l_{y}]$.

Relatsioonilised domeenid

Kolmemõõtmeline kumer hulktahukas kirjeldamaks kolme muutuja võimalike väärtusi. Iga muutuja võib olla null, kuid kõik kolm ei saa korraga olla nullid. Seda omadust ei saa intervallide domeenis kirjeldada

Järgnevas programmis on muutuja z väärtus alati null:

y = x;
z = x - y;

Kasutades intervallide domeeni ja eeldades, et muutuja x väärtus on algul lõigus $[0,1]$, leitakse, et muutuja z väärtus on lõigus $[-1,+1]$. Tulemus pole vale, kuid mitte nii täpne, kui võiks tahta, sest see domeen ei arvesta lahutamisel muutujate omavahelist seost, mistõttu nimetatakse domeeni mitterelatsiooniliseks.

Relatsionaalsed domeenid, mis muutujatevahelisi seoseid arvestavad, on näiteks:

• kongurentsiseosed täisarvudel,
• kumerad hulktahukad,
• kaheksanurgad.

Muud domeenid

Lisaks täisarvuliste väärtustele võib analüüsida ka muud tüüpi andmeid ja muid programmi omadusi, näiteks:

• korduvaid või üleliigseid arvutusi,
• mitmelõimeliste programmides lukke ja andmejookse.

Välislingid

• Patrick Cousot' veebileht abstraktse interpretatsiooni kohta