Egy fejlesztés során tekintélyes időt fordítunk az alkalmazás megtervezésére: arra, hogy pontosan specifikáljuk, majd dokumentáljuk a moduljainak, osztályainak, metódusainak működését. A tesztek implementálása azonban mindezen erőfeszítések ellenére sem spórolható meg. Pedig egy teszt nem más, mint az informális specifikáció formális megvalósítása. A programozók nem szeretik ugyanazt a dolgot kétszer megcisnálni, és a tesztelés kapcsán mégis rá vannak erre kényszerítve. Mi lenne, ha egy formális specifikációs nyelvet használva leírhatnánk az alkalmazás viselkedését, majd ezt a formális leírást arra használnánk, hogy bebizonyítsuk az alkalmazás helyességét? Hát tesztelés biztosan nem...

A Java Modeling Language

A Java Modeling Language [1] használatával formálisan leírható a Jáva modulok (osztályok) viselkedése. A nyelv könnyen megtanulható és használható, leírást anotációkon keresztül kell megadnia a fejlesztőknek. Ezenfelül számos eszköz támogatja a statikus analízist és verifikációt.

Talán az egyik leginkább használható eszköz David Cok és Joe Kikiry Extended Static Checker for Java version 2 (ESC/Java2) nevű helyességbizonyító eszköze [2]. Az eszköz első verzióját még a Compaq Researchnél fejlesztették ki, miután a Compaq leállította a projektet, Cok és Kiniry folytatta a munkák, és fejlesztette ki az ESC/Java második verzióját. Az ESC/Java2 tehát a JML annotációkkal ellátott Java programok helyességét próbálja bebizonyítani pusztán statikus elemzéssel.

Tehát, elméletileg, rendelkezésünkre áll az az eszköz, amellyel leírhatjuk az alkalmazásunk viselkedését és bebizonyíthatjuk az implementáció helyességét. És ennél többet nem is kell tennünk. Az implementációtol eltekintve munka véget is ér a specifikáció elkészülte után, megszabadultunk a tesztek készítésétől. Hát nem nagyszerű?! Nos, elméletben igen.

Lássuk csak a mindennapi napi gyakorlatot!

JML specifikációk készítése

Ugorjunk a mélyvízbe és tegyük feleslegessé a SAMS API TCK tesztjeinek egy részét [3]. A SAMS API egy üzenetküldésre szolgáló programozói könyvtár, amelynek segítségével a programozó SMS és MMS üzeneteket hozhat léétre, küldhet, vagy fogadhat [4]. A specifikációval együtt SAMS Referencia Implementáció és TCK letölthető a Forum Nokia oldaláról [5][6].

Az RI és a TCK telepítése után kezdjük el formális módon leírni az API néhány moduljának viselkedését. Kezdjük mondjuk a javax.sams.messaging.sms.TextMessage interface-szel és a hozzá tartozó impleemntációs osztállyal:

public interface TextMessage extends SmsMessage {
  public static final int VOICEMAIL_WAITING = 0;
  public static final int FAX_WAITING = 1;
  public static final int EMAIL_WAITING = 2;
  public static final int OTHER_WAITING = 3;
  public String getText();
  public void setText(String text) 
    throws InvalidArgumentException, MessageSizeExceededException;

  public void setMessageWaitingIndicator(
		int type, int count, boolean store)
    throws InvalidArgumentException, MessageSizeExceededException;

  public int getMessageWaitingCount(int type) 
    throws InvalidArgumentException;

  public boolean getMessageWaitingStore(int type) 
    throws InvalidArgumentException;

  public int[] getMessageWaitingTypes();
}

Láthatjuk, hogy a TextMessage interface nem más, mint a szöveges SMS üzenetek egy meglehetősen egyszerű konténere. Specififikáljuk getText() metódus viselkedését, melynek API specifikációja a következőképpen szól:

Returns the content of the text message as a String. Returns null if the content has not been set.

Returns:
  the content of the message or null

Nos, ezt elég könnyű JML-ben specifikálni:

/*@
  @ public normal_behavior
  @   _text_set ==> \result == _message_text; 
  @ // Returns the content of the text message as a String.
  @   !_text_set ==> \result == null; 
  @ // Returns null if the content has not been set.
  @*/
public String getText();

Emellett fel kell vennünk egy un. modell mezőt, amely tartalmazza az üzenet szövegét, valamint egy specifikációs változót (ghost mezőt), mely megmondja, hogy az üzenet szövege be van-e már állítva:

//@ ghost boolean _text_set = false;
//@ instance model String _message_text;

Egy JML model mezőnek lennie kell egy aktuális reprezentációjának a megfelelő implementációs osztályban, esetünkben ez az implementációs osztály a com.nokia.sams.messaging.sms.TextMessageImpl lesz.

Rendben, végeztünk a getText()-tel, most pedig specifikálnunk kell specifikálnunk kell a setText(String) viselkedését is!

A setText(String) API specifikációja a következőképpen szól:

Sets the content of the text message.

The length of the content depends on the character set encoding and whether there are optional headers. 
If the content does not fit into one message, it will be automatically split into multiple message segments.

The maximum number of segments in the message can be set by setMaxSegmentCount method. 
If the message size will exceed the maximum count, an MessageSizeExceededException will be thrown.

The text may be set to null, which indicates an empty content.

Parameters:
  text - the content text of the message

Throws:
  InvalidArgumentException 
    - if the text is invalid 
    (e.g. it includes unsupported characters)
  MessageSizeExceededException 
    - if content makes the message too long

See Also:
  SmsMessage.setMaxSegmentCount(int)

A TCK assertion dokumentáció (ld. JSR212_TCK_J2EE\doc\SAMS_TCK_Assertions_v11.doc) további, informális leírással szolgál a metódus elvárt működéséről:

Assertions:

 Assertion1:  
  Sets the content of the text message.

 Assertion2:  
  If the message became oversized, 
  a MessageSizeExceededException 
  will be thrown when the message is tried-to-be-sent.

 Assertion3:  
  InvalidArgumentException is thrown if the text is invalid 
  (e.g. it includes unsupported characters).

Equivalence class partitioning



text


Expected result





valid


Sets the content of the text message.





invalid (oversized)


MessageSizeExceededException


Boundary value analysis



text


Expected result





null, ""


Sets the content of the text message.





Text with length of MaxSegmentCount * SegmentSize


Sets the content of the text message.





Text with length of MaxSegmentCount * SegmentSize + 1


MessageSizeExceededException

Az új JML viselkedésleírás megfelel az egyes assertion-öknek:

/*@ public normal_behavior
  @   ensures (_message_text == text || _message_text == null) 
  @       && _text_set; // Assertion1
  @ also
  @ public exceptional_behavior
  @   signals (Exception e) (e instanceof InvalidArgumentException
  @      || e instanceof MessageSizeExceededException) &&
  @     _text_set == \old(_text_set) 
  @     && _message_text == \old(_message_text); 
  @     // Assertion2 and Assertion3
  @*/
public void setText(String text) 
  throws InvalidArgumentException, MessageSizeExceededException; 

A formális leírás némileg (nagyon is) megengedő az Assetion2 és Assetion3 formulák esetében, azonban a leírás a későbbiekben még szigorítható. Ettől eltekintve a leírás pontosan azt kifejezi azt, amit az API specifikáció is előír.

Reprezentáció

Tehát adott egy setter és egy getter metódus, melyek specifikációját sikeresen elkészítettük. Az implementáció helyességének ellenörzése előtt meg kell adnunk a _message_text modell mező reprezentációját a TextMessageImpl implementációs osztályban. Ez igazán könnyű feladat, miután a TextMessageImpl osztály éppen egy Stringben tárolja az üzenet szövegét.

public class TextMessageImpl extends SmsMessageImpl implements TextMessage {
  //@ represents _message_text <- messageText;
  [...]
  private String messageText = null;
  [...] 
} 

Foglalkoznunk kell a még a _text_set specifikációs mezővel is. Jelen állapotában ugye a reprezentáció nélküli _message_text mezőhöz hasonlóan nem definiált az értéke. A _text_set mező értékét létrehozáskor false-ra állítjuk, majd amikor az üzenet szövegét valaki megadja, a mező értékét true-ra állítjuk:

public void setText(String text) 
  throws InvalidArgumentException, MessageSizeExceededException {
    [...]
    //@ set _text_set = true;
}

Eljött az igazság pillanata!

Mire jutottunk idáig? Az API specifikációnak megfelelően formális leírást adtunk a getText() és a setText(String) metódusokhoz, valamint megadtuk a model és specifikációs mezők reprezentációját. Lássuk hát, vajon a SAMS Referencia Implementáció (RI) megfelel-e a specifikációnak. (Megtehetnénk, hogy egyszerűen futtatjuk a TCK-t, de ez a cikk mégiscsak a formális specifikációs módszerekről szól, nem igaz? Szóval talán majd máskor...)

Ahhoz, hogy ellenőrizhessük a RI heleysségét, el kell indítanunk az ESC/Java2 elemzőt az JSR212_RI könyvtárban:

$ escj -cp src/ com.nokia.sams.messaging.sms.TextMessageImpl

[...]

com.nokia.sams.messaging.sms.TextMessageImpl: 
  getText() ...
    [0.061 s 12850496 bytes]  passed

com.nokia.sams.messaging.sms.TextMessageImpl: 
  setText(java.lang.String) ...
src/com/nokia/sams/messaging/sms/TextMessageImpl.java:61: 
  Caution: Not checking body of anonymous 
class (subclass of Rollback)
        new Rollback() {
                       ^
    [0.504 s 13376272 bytes]  passed

[...]

Hm, ez nem hangzik valami jól. Valamit kezdenünk kell az anonim osztályokkal! Hogy minál hamarabb láthassuk az eredményt, egyszerűen belegányoljuk a problémás kódrészletet egy új metódusba:

public void setText(String text) 
  throws InvalidArgumentException, MessageSizeExceededException {
    String oldValue = messageText;

    messageText = text;

    if (!check((messageText != null)
     && ((oldValue == null) || ((oldValue != null) 
     && (oldValue.length() < messageText.length()))), oldValue)) {
      messageText = oldValue;
    }

  //@ set _text_set = true;
}

private boolean check(boolean b, String oldValue)  throws 
InvalidArgumentException, MessageSizeExceededException {
  try {
    checkSegmentCount(b, oldValue,
      new Rollback() {
        public void rollback(Object data) {} });
    return true;
  } catch (Exception e) {
    return false;
  }
}

Ismét futtassuk le az ESC/Java2-t:

[...]

com.nokia.sams.messaging.sms.TextMessageImpl: 
  getText() ...
    [0.061 s 12822536 bytes]  passed

com.nokia.sams.messaging.sms.TextMessageImpl: 
  setText(java.lang.String) ...
    [0.506 s 12873120 bytes]  passed

com.nokia.sams.messaging.sms.TextMessageImpl: 
  check(boolean, java.lang.String) ...
src/com/nokia/sams/messaging/sms/TextMessageImpl.java:69: 
  Caution: Not checking body of anonymous 
class (subclass of Rollback)
                  new Rollback() {
                                 ^
    [0.103 s 12967928 bytes]  passed

[...]

Eljött a TCK pillanata!

Siker! Az ESC/Java2 bebizonyította, hogy a SAMS RI helyes! Kinek van szüksége még TCK-ra?

Ahhoz, hogy megnyugtassuk magunkat arról, hogy az RI valóban helyes, rontsjuk el az implementációt:

public String getText() {
  return "foo";
}

Az ESC/Java2 ítélete:

com.nokia.sams.messaging.sms.TextMessageImpl: getText() ...
---------------------------------------------------------------------
src/com/nokia/sams/messaging/sms/TextMessageImpl.java:47: 
Warning: Postcondition possibly not established 
(Post)   }
         ^
Associated declaration is "src/javax/sams/messaging/sms/TextMessage.java", 
line 57, col 6:
             ensures  _text_set ==> \result == _message_text;
             ^
Execution trace information:
    Executed return in "src/com/nokia/sams/messaging/sms/TextMessageImpl.java", 
  line 46, col 4.

---------------------------------------------------------------------

Remek! Az eszköz kiszúrta a helytelen viselkedést!

Azonban, ha a következőképpen rontjuk el a kódot:

public String getText() {
  return messageText + "foo";
}

Az ESC/Java2 hibásan jónak ítéli az implementációt.

com.nokia.sams.messaging.sms.TextMessageImpl: getText() ...
    [0.381 s 13123600 bytes]  passed

És ez az a pillanat, amikor ismét elkezdhetünk, modul, és funkcionális teszteket irogatni.

Összegzés

A JML [1] leíró nyelvet használva megpróbáltuk leírni a JSR212 (SAMS) szabvány két egyszerű metódusának működését, és az ESC/Java2 [2] felhasználásával megpróbáltuk bebizonyítani az implementáció helyességét. Egy átlagos Java programozó gyorsan elsajátíthatja a JML nyelv használatát: a nyelv széles körben jól ismert fogalmakat használ operál (elő- és utófeltételek, invariánsok, reprezentációs függvények, annotációk, stb.), emellett a lehető legjobban követi a Java nyelv szintaxisát és szemantikáját. A JML kitűnő eszköznek bizonyult arra, hogy pontos formális leírást adjunk a Java alkalmazások működéséről.

Potenciálisan egy JML leírás elkészítése a statikus helyességbizonyítási folyamat első lépésének tekinthető. Illetve pontosabban fogalmazva: első lépésének tekinthető lenne. Noha az ESC/Java2 tervezett képességei bíztatók, az eszköz ezen képességeknek valójában még nincsen a birtokában, és jelenleg nincs olyan eszköz a piacon, amely feleslegessé tenné a modul és funkcionális tesztelést.

És igen, tesztelj, mivel úgyse tudsz bizonyítani!

[Ugrás az oldal tetejére]

Referenciák:

[1] JML Home Page: http://www.jmlspecs.org

[2] ESC/Java2: http://secure.ucd.ie/products/opensource/ESCJava2/

[3] Java Community Process: http://www.jcp.org

[4] JSR 212: Server API for Mobile Services: http://www.jcp.org/en/jsr/detail?id=212

[5] SAMS RI: jsr212 ri j2ee v11 installer

[6] SAMS TCK: jsr212 tck j2ee v11 installer