A Haskell programozási nyelv

Helyességbizonyítás



A Haskell nyelv egyik leghasznosabb újdonsága az, hogy a programszöveg formázásának szintaktikai jelentése van - és nem csak annyi, hogy a sor végére nem kell kiírni a pontosvesszőt, mint Eiffelben. Azaz a fordító figyeli a szöveg tördelését is, és ez erősen befolyásolja a szöveg értelmezését. Éppen ezért a Haskell programok kinézete sokkal egységesebb, mint más programnyelvek esetében. Persze lehetőség van a tagolás figyelmen kívül hagyására is, ekkor a szintaxis leginkább a C nyelvére hasonlít - ezt azonban nagyon ritkán csinálják.

A Haskell nyelv nem rendelkezik külön helyességbizonyító eszközökkel. Tapasztalatom szerint nem is nagyon van rá szükség, mivel egyrészt a típusellenőrző rendszere nagyon jól működik, másrészt mert a Haskellben való programozás eleve olyan gondolkodásmódot igényel, ami közel áll a módszertanban tanult gondolkodásmódhoz, ezért a programok kezdettől jobban átgondoltak. Ráadásul a Haskell szintaxisa is olyan, hogy az közel áll a matematikai jelölésekhez, így a programozás során tulajdonképpen elkerülhetetlen, hogy az ember részletes, formalizált specifikációt írjon, az implementációt pedig az esetek nagy részében elvégzi maga a Haskell.

Lefedettség tesztelés

A lefedettség tesztelés (coverage testing) annak a megállapításában segít, hogy elegendő tesztesetet készítettünk-e a programunkhoz. Azaz tény hogy nem helyességbizonyító eszközről fogunk beszélni, ám a gyakorlatban használható eszközről lesz szó.

A GHC fordító 6.8 verziótól kezdve tartalmazza a hpc lefedettség tesztelőt. A hpc működési elve a következő: Lefordítjuk a programot a ghc megfelelő kapcsolójával, ezután futtatjuk a teszteket. A tesztek futtatása során keletkezett adatokból HTML oldalt készíthetünk. Ezen látszani fog a program forrása, külön kiemelve azokat a részeket amik egyetlen teszt során sem értékelődtek ki.