3.2. Statikus elemzés

A statikus elemzés fehérdobozos teszt, hiszen szükséges hozzá a forráskód. Néhány esetben, pl. holtpont ellenőrzés, elegendő a lefordított köztes kód (byte kód). A statikus elemzés azért hasznos, mert olyan hibákat fedez fel, amiket más tesztelési eljárással nehéz megtalálni. Például kiszűrhető segítségével minden null referencia hivatkozás, ami az alkalmazás lefagyásához vezethet, ha benne marad a programban. Az összes null referencia hivatkozás kiszűrése dinamikus technikákkal (pl. komponens teszttel vagy rendszerteszttel) nagyon sok időbe telne, mert 100%-os kódlefedettséget kellene elérnünk.

A statikus elemzés azt használja ki, hogy az ilyen tipikus hibák leírhatók egyszerű szabályokkal, amiket egy egyszerű kódelemző (parser) gyorsan tud elemezni. Például null referencia hivatkozás akkor lehetséges, ha egy „a = null;” értékadó utasítás és egy „a.akármi;” hivatkozás közt van olyan végrehajtási út, ahol az „a” referencia nem kap null-tól különböző értéket. Ugyan ezt lehet dinamikus technikákkal is vizsgálni, de ahhoz annyi tesztesetet kell fejleszteni, ami minden lehetséges végrehajtási utat tesztel az „a = null;” és az „a.akármi;” közt.

A forráskód statikus elemzésnek két változata ismert, ezek:

  1. statikus elemzés csak a forráskód alapján,

  2. statikus elemzés a forráskód és modell alapján.

Ezen túl lehetséges a dokumentumok statikus elemzése is, de ezekre nem térünk ki.

A következő hiba típusokat könnyebb statikus elemzéssel megtalálni, mint más technikákkal:

  1. null referenciára hivatkozás,

  2. tömbök túl vagy alul indexelése,

  3. nullával való osztás,

  4. lezáratlan adat folyam (unclosed stream),

  5. holtpontok (deadlock),

  6. kiéheztetés (starvation).

Az egyes eszközök lehetnek specifikusak, mint pl. a holtpont keresők, illetve általánosak, mint pl. a FindBugs.

3.2.1. Statikus elemzés csak a forráskód alapján

Azok az elemzők, amelyek csak a forráskódot használják fel az elemzéshez, azok nagyon hasznosak olyan szempontból, hogy nem igényelnek plusz erőfeszítést a programozóktól a specifikáció megírásához. Ilyen eszköz például a FindBugs. Ezeket az eszközöket csak bele kell illeszteni a fordítás folyamatába. Ezután a statikus elemző felhívja a figyelmünket a tipikus programozói hibákra. Ezek általában programozási nyelv specifikusak, de léteznek nyelv függetlenek, pl. a Sonar vagy a Yasca rendszer, amelyek egy-egy plugin segítségével adaptálhatóak a kedvenc nyelvünkhöz.

Jelen jegyzetben a FindBugs használatát fogjuk bemutatni Eclipse környezetben. Először telepíteni kell a FindBugs plugint. Ehhez indítsuk el az Eclipse rendszert, majd válasszuk a Help -> Install New Software… menüt. A megjelenő ablakban adjuk hozzá a plugin források listájához az alábbi linket az Add gombbal: http://findbugs.cs.umd.edu/eclipse. Ezután néhány Next gomb és a felhasználási feltételek elfogadása után a rendszer elkezdi installálni a FindBugs plugint. Ez néhány percet vesz igénybe, ami után újraindul az Eclipse. Ezután már használhatjuk a FindBugs-t.

A használatához válasszunk ki egy projektet, majd a helyi menüben válasszuk a Find Bugs -> Find Bugs menüt. Ez egyrészt megkeresi azokat a sorokat, amelyek valamilyen szabálynak nem felelnek meg, másrészt átvisz minket a FindBugs perspektívába. Ha talál hibákat, akkor ezeket bal oldalon egy kicsi piros bogár ikonnal jelzi. Ha ezekre ráállunk vagy rákattintunk, akkor láthatjuk, milyen típusú hibát találtunk. Ezekről részletes információt is kérhetünk, ha a FindBugs perspektíva Bug Explorer ablakában kiválasztjuk valamelyiket.

Az egyes hibák ellenőrzését ki/be lehet kapcsolni a projekt Properties ablakának FindBugs panelén. Itt érdemes a Run atomatically opciót bekapcsolni. Így minden egyes mentésnél lefut a FindBugs. Ebben az ablakban az is látható, melyik hiba ellenőrzése gyors, illetve melyik lassú. Például a null referenciára hivatkozás ellenőrzése lassú.

Nézzünk néhány gyakori hibát, amit megtalál a FindBugs az alapbeállításaival:

   public int fact(int n) { return n*fact(n-1); }
       

Itt a „There is an apparent infinite recursive loop” figyelmeztetést kapjuk nagyon helyesen, hiszen itt egy rekurzív függvényt írtunk bázis feltétel nélkül, és így semmi se állítja meg a rekurziót.

  Integer i = 1, j = 0;
  if(i == j) System.out.println("ugyanaz");
         

Ebben a példában a „Suspicious comparison of Integer references” figyelmeztetést kapjuk. Ez azért van, mert referenciák egyenlőségét ugyan tényleg a dupla egyenlőségjellel kell vizsgálni, de a mögöttük lévő tartalom egyenlőségét az equals metódussal kell megvizsgálni. Tehát ez egy lehetséges hiba, amit érdemes a fejlesztőknek alaposan megnézni.

 int i = 0;
 i = i++;
 System.out.println(i);

Itt több hibát is kapunk: „Overwritten increment” és „Self assignment of local variable”. Az első hiba arra utal, hogy hiába akartuk növelni az i változó értékét, az elvész. A második hiba azt fejezi ki, hogy egy változót önmagával akarunk felülírni.

Nézzünk olyan esetet is, aminél hibásan ad figyelmeztetést a FindBugs:

 public static void main(String[] args){
 Object o = null;
         int i = 1;
        if(i == 1) o = "hello";
        System.out.println(o.toString());
 }

A fenti esetre a „Possible null pointer dereference of o” hibát kapjuk, habár egyértelműen látszik, hogy az o értéket fog kapni, hiszen igaz az if utasítás feltétele. Ugyanakkor a FindBugs rendszer nem képes kiszámolni a változók lehetséges értékeit az egyes ágakon, hiszen nem tartalmaz egy automatikus tételbizonyítót. Ezzel szemben a következő alfejezetben tárgyalt ESC/Java2 eszköz képes erre, hiszen egy automatikus tételbizonyítóra épül.

3.2.2. Statikus elemzés a forráskód és modell alapján

Ebben az esetben a forráskód mellett van egy modellünk is, ami leírja, hogyan kellene működnie a programnak. A program viselkedése ilyen esetben elő- és utófeltételekkel, illetve invariánsokkal van leírva. Ezt úgy érjük el legkönnyebben, hogy kontraktus alapú tervezést (design by contract) használunk. Ez esetben minden metódusnak van egy kontraktusa, amely a metódus elő- és utófeltételében ölt testet. A szerződés kimondja, hogy ha a metódus hívása előtt igaz az előfeltétele, akkor a metódus lefutása után igaznak kell lennie az utófeltételének. Az invariánsok általában osztály szintűek, leírják az osztály lehetséges belső állapotait. A program viselkedését legegyszerűbben assert utasításokkal írhatjuk le.

Egy példa assert használatára:

  public double division(double a, double b){
         assert(b!=0.0);
          return a / b;
  }

A fenti példában azt feltételezzük, hogy a metódus második paramétere nem nulla. A program kódjában a feltételezéseinket assert formájában tudjuk beírni Java esetén. Java esetén az assert utasítások csak akkor futnak le, ha a JVM-et a –enableassert vagy az egyenértékű –ea opcióval futtatjuk, egyébként nincs hatásuk.

C# esetén a fenti példa megfelelője ez:

  public double division(double a, double b)
  {
  System.Diagnostics.Debug.Assert(b != 0.0);
        return a / b;
  }

Az Assert csak akkor fog lefutni, ha a Debug módban fordítjuk az alkalmazást.

A program viselkedését legegyszerűbben assert utasítások lehet leírni, de lehetőségünk van magas szintű viselkedés leíró nyelvek használatára, mint például a JML (Java Modeling Language) nyelv. Ez esetben magas szintű statikus kód ellenőrzést (Extended Static Checking, ESC) tudunk végezni az ESC/Java2 program segítségével.

Egy példa JML használatára:

   public class BankSzámla {
          private /*@ spec_public @*/ int balansz = 0;
           private /*@ spec_public @*/ boolean zárolt = false; 
           //@ public invariant balansz >= 0;        
           //@ requires 0 < összeg;
           //@ assignable balansz;
           //@ ensures balansz == \old(balansz) + összeg;
           public void betesz(int összeg) { balansz += összeg; }
   
           //@ requires 0 < összeg && összeg <= balansz;
           //@ assignable balansz;
           //@ ensures balansz == \old(balansz) - összeg;
           public void kivesz(int összeg) { balansz -= összeg; }
   
           //@ assignable zárolt;
          //@ ensures zárolt == true;
           public void zárol() { zárolt = true; }
   
           //@   requires !zárolt;
           //@   ensures \result == balansz;
           //@ also
           //@   requires zárolt;
           //@   signals_only BíankingException;
           public /*@ pure @*/ int getBalansz() throws BankingException {
                   if (!zárolt) { return balansz; }
                   else { throw new BankingException("Zárolt a számla"); }
           }
   }

Ebből a kis példából lehet látni, hogy a JML specifikációt megjegyzésbe kell írni, amely az @ jellel kezdődik. A spec_public kulcsszóval teszünk láthatóvá egy mezőt a JML specifikáció számára. Az invariant kulcsszó után adjuk meg az osztály invariánsát, amelynek minden (nem helper) metódus hívás előtt és után igaznak kell lennie. Az előfeltételt a requires kulcsszó után kell írni. Maga a feltétel egy szabályos Java logikai kifejezés. A kifejezésben lehet használni JML predikátumokat is. Az utófeltétel kulcsszava az ensures. Lehet látni, hogy az utófeltételben lehet hivatkozni a visszatérési értékre a \result JML kifejezéssel. Az \old(x) JML kifejezés az x változó metódus futása előtti értékére hivatkozik. Az assignable kulcsszó segítségével úgynevezett keretfeltétel (frame condition) adható, amiben felsorolhatom, hogy a metóduson belül mely mezők értékét lehet megváltoztatni. Ha egyik mező értékét sem változtathatja meg a metódus, akkor azt mondjuk, hogy nincs mellékhatása. Az ilyen metódusokat a pure kulcsszóval jelöljük meg. Elő- és utófeltételben csak pure metódusok hívhatok. Az also kulcsszó esetszétválogatásra szolgál. A signals_only kulcsszó után adható meg, hogy milyen kivételt válthat ki a metódus.

Az fenti példában van egy BankSzámla osztályunk, amelyben a balansz mező tárolja, hogy mennyi pénzünk van. Az invariánsunk az fejezi ki, hogy a balansz nem lehet negatív. Négy metódusunk van. A metódusoknál megadjuk elő- és utófeltételüket természetes nyelven:

  1. betesz(összeg)

  2. Előfeltétel: Az összeg pozitív szám, mert nulla forintot nincs értelme betenni, negatív összeget pedig nem szabad.

  3. Keret feltétel: Csak a balansz mezőt írhatja.

  4. Utófeltétel: A balanszot meg kell növelni az összeggel, azaz az új balansz a régi balansz plusz az összeg.

  5. kivesz(összeg)

  6. Előfeltétel: Az összeg pozitív szám, mert nulla forintot nincs értelme kivenni, negatív összeget pedig nem szabad. Továbbá az összeg kisebb egyenlő, mint a balansz, mert a számlán lévő összegnél nem lehet többet felvenni.

  7. Keret feltétel: Csak a balansz mezőt írhatja.

  8. Utófeltétel: A balanszot csökkenteni kell az összeggel, azaz az új balansz a régi balansz mínusz az összeg.

  9. zárol()

  10. Előfeltétel: Nincs, azaz mindig igaz.

  11. Keret feltétel: Csak a zárolt mezőt írhatja.

  12. Utófeltétel: A zárolt mezőnek igaznak kell lennie.

  13. getBalansz()

  14. Két esetet különböztetünk meg, ahol az előfeltételek kizárják egymást.

  15. Előfeltétel: A számla nem zárolt.

  16. Utófeltétel: A visszatérési érték megegyezik a balansz értékével.

  17. Előfeltétel: A számla zárolt.

  18. Kivétel: Zárolt számla nem kérdezhető le, ezért BankingException kivételt kell dobni.

  19. Keret feltétel: Mindkét esetben egyik mező sem írható, tehát ez a metódus „pure”.

A JML nyelvhez több segédeszköz is létezik. Az első ilyen az Iowa State University JML program. Ez a következő részekből áll:

  1. jml: JML szintaxis ellenőrző

  2. jmlc: Java és JML fordító, a Java forrásban lévő JML specifikációt belefordítja a bájtkódba.

  3. jmlrac: a jmlc által instrumentált bájtkódot futtató JVM, futtatás közben ellenőrzi a specifikációt, tehát dinamikus ellenőrzést végez.

Nekünk a JML 5.4 és 5.5 verziót volt szerencsénk kipróbálni. Sajnos ezek csak a Java 1.4 verzióig támogatják a Java nyelvet. Nem ismerik például a paraméteres osztályokat. Ha simán hívjuk meg a jmlc parancsot, akkor rengeteg információt kiír, ami esetleg elfed egy hibát. Ezért érdemes a -Q vagy a -Quite opcióval együtt használni. A BankSzámla példát a következő utasításokkal lehet ellenőrizni, hogy megfelel-e specifikációjának:

jmlc -Q BankSzámla.java

jmlrac BankSzámla

Persze ehhez a BankSzámla osztályba kell írni egy main metódust is, hiszen az a belépési pont.

Második példa:

     //******* AbstractAccount.java *******  
     package bank3;  
     public abstract class AbstractAccount {  
             //@ public model int balance;  
             //@ public invariant balance >= 0;  
  
             //@ requires amount > 0;  
             //@ assignable balance;  
             //@ ensures balance == \old(balance + amount);  
             public abstract void credit(int amount);          
             //@ requires 0 < amount && amount <= balance;  
             //@ assignable balance;  
             //@ ensures balance == \old(balance) - amount;  
             public abstract void debit(int amount);  
             //@   ensures \result == balance;  
             public abstract /*@ pure @*/ int getBalance();  
     }  
     //******* Account.java *******  
     package bank3;  
     public class Account extends AbstractAccount{          
             private /*@ spec_public @*/ int balance = 0; //@ in super.balance;  
             //@ private represents super.balance = balance;  
             public void credit(int amount) { balance += amount; }  
             public void debit(int amount) { balance -= amount; }  
             public int getBalance() { return balance; }  
     }  
            

Ez a példa azt mutatja meg, hogyan lehet már az interfészben vagy az absztrakt ős osztályban specifikálni az elvárt viselkedést. Ehhez egy modell mezőt kell definiálni az ősben (vagy az interfészben) a „model” kulcsszóval. A konkrét gyermekben az ősben specifikált viselkedést meg kell valósítani. Ehhez meg kell mondani, hogy melyik konkrét mező valósítja meg a modell mezőt. Ez a  „represents” kulcsszó használatával lehetséges.

A fenti példát a következő utasításokkal lehet ellenőrizni:

 jmlc -Q bank3/*.java

jmlrac bank3.Account

Persze ehhez a Account osztályba kell írni egy main metódust is, hiszen az a belépési pont.

Harmadik példa:

              //******* Timer.java *******  
     package bank4;  
     public interface Timer{  
       //@ public instance model int ticks;  
       //@ public invariant ticks >= 0;  
       //@ assignable this.ticks;  
       //@ ensures this.ticks == ticks;  
       void setTimer(int ticks);  
     }  
     //******* Dish.java *******  
     package bank4;  
     public class Dish implements Timer{  
       private /*@ spec_public @*/ int timer; //@ in ticks;  
       //@ private represents ticks = timer;  
       public void setTimer(int timer) { this.timer = timer;}  
     }  
            

Ez a példa azt mutatja meg, hogyan kell modell mezőt létrehozni az interfészben. Mindent ugyanúgy kell csinálni, csak a „model” kulcsszó elé be kell írni az „instance” kulcsszót, ami azt fejezi ki, hogy a modell változó példány szintű. Erre azért van szükség, mert egyébként Javában minden interfész mező statikus.

Láttuk, hogy a specifikáció dinamikus ellenőrizhető az Iowa State University JML programmal. Szerencsére lehetséges a statikus ellenőrzés is az ESC/Java2 programmal.

Az ESC/Java2 (Extended Static Checker for Java2) egy olyan segédeszköz, amely ellenőrizni tudja, hogy a Java forrás megfelel-e a JML specifikációnak. Az ESC/Java2 hasonlóan a FindBugs programhoz figyelmezteti a programozót, ha null referenciára hivatkozik, vagy más gyakori programozói hibát vét. Erre akkor is képes, ha egy JML sor specifikációt se írunk. Nyilván, ha kiegészítjük a kódunkat JML specifikációval, akkor sokkal hasznosabban tudjuk használni.

Az ESC/Java2 program is csak a Java 1.4 verziójáig támogatja a Java nyelvet. Ez is telepíthető Eclipse pluginként a http://kind.ucd.ie/products/opensource/Mobius/updates/ címről.

Miután feltelepítettük két új perspektívát kapunk, a Validation és a Verification nevűt. Az elsőben 3 új gombban bővül a menüsor alatti eszköztár. Ezek a következőek: JML, JMLC, és a JMLRAC gomb, amelyek az azonos nevű segédprogramot hívják az Iowa State University JML programcsomagból.

A második perspektívában 5 új gombot kapunk. Ezek közül a legfontosabb az első, amely elindjtja a ESC/Java2 ellenőrző programot. A többi gomb balról jobbra haladva a következők: jelölők (jelölőknek nevezzük a hiba helyét jelölő piros ikszet) törlése, ugrás jelölőre, ellenörzés engedélyezése, ellenőrzés tiltása. Ezeket nem találtuk különösebben hasznosnak. Ami hasznos volt számunkra az az ESC/Java2 menüben található Setup menü. Itt lehet bekapcsolni az automatikus ellenőrzést, aminek hatására minden egyes mentés után lefut az ESC/Java2.

Nézzünk egy egyszerű példát, amikor JML specifikáció nélkül is hibát fedez fel a kódunkban az ESC/Java2.

   package probe;
   public abstract class Decorator extends Car {
           Car target;
           public int getSpeed(){
                   return target.getSpeed();
           }
            

Itt az ötödik sorra azt a hibát kapjuk, hogy „Possible null dereference (Null)”. Ez a figyelmeztetés teljesen jogos, segíti a programozót kijavítani egy hibát.

Nézzük meg azt a példát, amivel a FindBugs nem boldogult:

  public static void main(String[] args){
   Object o = null;
           int i = 1;
           if(i == 1) o = "hello";
           System.out.println(o.toString());
   }

Erre az ESC/Java2 semmilyen hibát nem ad. Ez azért lehetséges, mert mögötte egy automatikus tételbizonyító áll, ami meg tudja nézni, hogy valamely feltétel igaz vagy sem az egyes lehetséges végrehajtási utakon.

Ugyanakkor a ESC/Java2-höz adott Simplify nevű automatikus tételbizonyító nem túl okos. Például nem tudja, hogy két pozitív szám szorzata pozitív, ezért ad hibát a következő példára:

     public class Main {  
              //@ requires n>=0;  
              //@ ensures \result > 0;  
             public int fact(int n){  
                     if (n==0) return 1;  
                             return n*fact(n-1);  
             }  
     }  
            

Itt az ESC\Java2 hibásan a „Postcondition possibly not established (Post)” figyelmeztetést adja, pedig a függvény tökéletesen betartja az utófeltételét. Szerencsére az ESC\Java2 alatt kicserélhető az automatikus tételbizonyító.