Attila Góbi edited modszerek.tex  about 8 years ago

Commit id: 99354b35da09ccbb1bd7d57ffad08e56138726e7

deletions | additions      

       

A fenti példa azt mutatja, hogy tetszőleges programtulajdonság vizsgálható és bizonyítható megfelelő típusrendszerrel. A programok statikus elemzésére egy másik módszer a programok absztrakt interpretációja. Ebben a módszerben a program viselkedését közelítjük úgy, hogy tulajdonképpen egy absztrakt állapottéren futtatjuk le. Ezt a megoldás gyakran használják fordítóprogramok a programok elemzésére (a control-flow és data-flow elemzés mellett).  Egy ilyen absztakt állapottér lehet a méretek felső korlátja. Ekkor az interpretáló függvényünk listákhoz a listák méretét rendeli. Elágazás esetén Ez  a módszer nem számítja ki a listák konkrét elemeit, csak azok méreteit, ezáltal egy közelítését adja a megoldásnak.  A fejlett típusrendszerek lehetővé teszik, hogy egy gazdanyelv segítségével megfogalmazzunk egy olyan programozási nyelvet, amelyet a gazdanyelv eszközeivel írunk le és a gazdanyelv típusrendszere ellenőriz.