Tézisfüzet

Bevezetés

A magas szintű nyelvek megjelenésével egyidőben jelen meg az igény arra, hogy a fordítóprogramok képesek legyenek fordítási időben bizonyos programtulajdonságokat elemezni. Ennek eleinte két fontos praktikus oka volt. Az egyik, hogy így írt programok futási ideje felvegye a versenyt az assembly nyelven írt programokkal, ami különösen fontos volt az akkori szűkös hardvereken. Másrész, akkoriban egy lyukkártyán leadott program esetében a fordítási hibát csak napokkal később kapta kézhez a programozó, célszerű volt tehát olyan fordítót írni, ami a lehető legtöbb hibáról és hibalehetőségről visszajelzést ad a fejlesztőnek, illetve a lehető legtöbb esetben megpróbálja kitalálni a programozó szándékát.

A helyzet mára teljesen megváltozott, a szoftverfejlesztő a fordítás kimenetéről általában perceken belül visszajelzést kap, az assembly nyelv pedig csak néhány speciális területen maradt használatban. Érdekes módon azonban a programok fordítási idejű elemzésének igénye egyáltalán nem csökkent. Ellenkezőleg, a mai szoftverek olyan méretűre nőttek, hogy azokat egy ember már képtelen átlátni, ennek következtében egyre nagyobb szerepe van a fordítónak abban, hogy az esetleges programhibákat már fordítási időben kiszűrje.

Másrészt az utóbbi években egyre több mindent szoftver vezérel (gondoljunk a mostanában terjedő Internet of Thingsre), és ezek egy része az emberi élet szempontjából is kritikus lehet. Egy ilyen példa a repülőgépek fly-by-wire rendszere, amelyek vezérlésének válaszidejére komoly garanciákat kell a gyártónak adnia. Ezeket rendkívül bonyolult szoftverekkel lehet csak validálni, az emberi munkával történő bizonyítás az időszüksége miatt komoly versenyhátrányt jelentene a tervezőknek.

Egy másik példa a mai beágyazott rendszerek. Egy mai készülék komoly hardver és szoftver együttese, ha valahogy meg tudjuk határozni a beágyazott rendszeren futó szoftver hardverigényét, azzal a gyártó a gyártási költségeit tudja optimalizálni, ami egy nagy példányszámban eladott termék esetén komoly megtakarítás lehet. A legtöbb ilyen termékben a gyártók a mai napig C nyelvet használnak, mert a programozóknak ezen a nyelven van a legnagyobb kontrollja a memóriahasználat felett. Sajnos egy modernebb nyelv hardverigénye és válaszideje (pl. szemétgyűjtés miatt) jóval kiszámíthatatlanabb, ezért ezekbe a szegmensekbe a modern nyelvek nem tudtak betörni annak ellenére, hogy a szoftverfejlesztési költségeket jelentősen csökkentené.

A fenti okok miatt kezdődött el a kutatása annak, hogy a programok erőforrásigényét elemző eszközökkel meg lehessen határozni. Ennek egyik lehetséges megoldása, hogy a kész, lefordított programot vizsgáljuk. Másik megoldás, hogy a program struktúráit vizsgáljuk magas szinten. Ennek egyik példája a fejlett típusrendszer, amelynek nagy előnye, hogy a program és a program elemzése lényegében ugyanabban a programkódban történik, külső eszköz nélkül. Más megközelítés az a módszer, amelyeket a fordítóprogramok használnak a programok elemzésére, pl. adatfolyam analízis és absztakt interpretáció.

Doktori dolgozatomban azzal foglalkoztam, hogy funkcionális nyelvekben (Haskell és F#) előforduló adatszerkezetek mérete hogyan határozható meg fordítási időben. Ez az információ közvetlenül segít a memóriahasználat kikövetkeztetésében, és közvetve felhasználható a futási idő elemzéséhez is.

Alkalmazott módszerek

Munkám során igyekeztem a legkülönbözőbb területekről a legkorszerűbb technológiákat és kutatási eredményeket felhasználni, így szükségesnek érzem egy szakaszt szentelni a felhasznált eszközök és módszerek rövid bemutatására. A következő bekezdésekben bemutatom, hogy mit nevezünk funkcionális nyelvnek, mik ezeknek a nyelveknek a jellemző típusrendszereik, és milyen programtulajdonságokat lehet ezekkel ellenőrizni. Ezután röviden ismertetem az absztrakt interpretációt is, mint alternatívát. A fenti módszerek implementálására használt beágyazás zárja az alkalmazott módszerek ismeretetését.

A kutatás során elsősorban tisztán funkcionális nyelvek elemzésével foglalkoztam. Funkcionális nyelvek alatt azokat a programozási nyelveket nevezzük, amelyek támogatják a funkcionális programozási paradigmát. Ez egy olyan deklaratív programozási stílus, amelyben támogatják a mellékhatásmentes függvények használatát, és az olyan adatszerkezeteket, amelyek nem módosíthatóak. Az ilyen nyelvekben a függvények első rendű elemként jelennek meg, és jellemző a magasabb rendű függvények használata, valamint a fejlett típusrendszer is.

A funkcionális nyelvek között kiemelkedő helyet foglalnak el a tisztán funkcionális nyelvek. Ezek a nyelvekre teljesül a hivatkozási helyfüggetlenség. Ez azt jelenti, hogy ha egy függvényt kétszer meghívok ugyanazzal a paraméterezéssel, az eredmény ugyanaz lesz. Ezek a nyelvek egyáltalán nem támogatnak változókat és állapotokat, valamint a mellékhatásokat (fájlrendszer használat, képernyőkezelés) is közvetett módon oldják meg. Egy ilyen elterjedt megoldás a monádok használata (pl. Haskell), ahol a monádok ábrázolják a külső vagy belső állapottal végezhető műveleteket, és a programunkat ezeknek a műveleteknek a segítségével építhetjük fel anélkül, hogy a hivatkozási helyfüggetlenség sérülne.

A tisztán funkcionális nyelvek az egyszerű és tiszta elméleti alapok miatt jól tárgyalhatóak, ennek egyik bizonyítéka, hogy a típusrendszerek legnagyobb eredményei is ezekhez a nyelvekhez köthetőek. A tisztán funkcionális nyelvek a gyakran statikus típusosak, azaz ellenőrzik, hogy a függvényeket megfelelő típusú paraméterekkel hívtuk-e meg.