From Wikipedia, the free encyclopedia
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:
Abstraktse interpretatsiooni teooria formaliseerisid prantsuse informaatikud Patrick Cousot ja Radhia Cousot 1970. aastate lõpus.[2][3] Esimene suuremahuline automaatne programmianalüüs abstraktse interpretatsiooni abil teostati Ariane 5 raketi koodil pärast selle esmalennu ebaõnnestumist 1996. aastal.[4]
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).[5]
Domeeni valik sõltub sellest, milliste programmi omaduste kohta informatsiooni otsitakse. Lisaks tuleb teha kompromiss selle täpsuse ja keerukuse vahel.
Täisarvuliste muutujate ja nende tehete lähendamiseks on abstraktsel interpreteerimisel mitmeid võimalusi.
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.[5]
Täpsemaks analüüsiks võib kasutada näiteks arvtelje lõike, kirjeldades iga muutuja võimalikke väärtusi täisarvude intervalliga . Sellistel lähendustel on võimalik defineerida aritmeetilised tehted, moodustades intervallaritmeetika.[6] Näiteks muutujate ja , mille intervallid on vastavalt ja , korral on
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 , leitakse, et muutuja z
väärtus on lõigus . 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:
Lisaks täisarvuliste väärtustele võib analüüsida ka muud tüüpi andmeid ja muid programmi omadusi, näiteks:
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.