Java Modeling Language.pdf

Programowanie

Java

Piotr Nazimek

Java Modeling Language

– te słowa są dla wielu programistów powo-

dem co najmniej kiepskiego humoru. Bo nie-

malże zawsze w trakcie tych „procesów” wychodzi na

jaw, że są jakieś niedociągnięcia. Pomijając fakt, że pi-

sanie dokumentacji (przed, po czy w trakcie tworzenia

aplikacji) jest nudne, to dodatkową nieprzyjemnością

jest poprawianie błędów. Skąd się one biorą? Wbrew

pozorom to niełatwe pytanie. Wiele z nich spowodowa-

nych jest niepoprawnym użyciem klasy lub metody, któ-

re wynika z niezrozumienia dokumentacji. Kolejne wy-

nikają z nieuwagi, niewiedzy lub wpadek innych osób.

Długo można dyskutować o przyczynach błędów w im-

plementacji, ale jedno jest pewne – zawsze winny jest

programista. Dlaczego? Ponieważ nie przetestował do-

brze swojego kodu. A czemu tego nie zrobił? Najczę-

ściej z braku czasu, choć można wymienić wiele innych

powodów: brak odpowiednich narzędzi, wiedzy, wypra-

cowanej metodyki testowania. Radą na to, przynajmniej

dla platformy Java, może być zastosowanie JML, czyli

Java Modeling Language .

Rysunek 1. Aplikacja jml-launcher

rzenia takiego modelu i jego implementacji aby nie wy-

stępowały w nim nigdy sytuacje powodujące narusze-

nie umowy (czyli błąd). Mając dobry model oraz imple-

mentację (niekoniecznie poprawną) chcielibyśmy tak ją

przetestować aby wykryć wszystkie ewentualne naru-

szenia. Najprostszym sposobem jest zamiana wszyst-

kich warunków na asercje w odpowiednich miejscach

kodu źródłowego. Niespełnienie asercji to naruszenie

umowy, czyli niepoprawna implementacja. Programi-

sta powinien dążyć do wyeliminowania wszystkich na-

ruszeń – wtedy zabezpieczenia (asercje) są zbędne

i będą mogły zostać usunięte.

Projektowanie związane umową

Projektowanie związane umową (ang. design by con-

tract, DBC ) jest jedną z wielu metodyk tworzenia opro-

gramowania. Jest to idea niemłoda, wywodzącą się

z logiki Hoare'a. Ogólnie rzecz ujmując stosowanie

DBC polega na określeniu: warunków początkowych

(ang. preconditions ) – są to warunki, które powinny być

spełnione przed wykonaniem np. danej instrukcji lub

metody; warunków końcowych (ang. postconditions ) –

są to warunki, które powinny być spełnione po wyko-

naniu np. danej instrukcji lub metody; niezmienników

(ang. invariants ) – są to warunki, które powinny być

spełnione w każdym momencie wykonania programu.

Ideę projektowania związanego umową można za-

wrzeć w zdaniu: „Jeżeli spełnione będą wymagania po-

czątkowe to na pewno spełnione zostaną wymaga-

nia końcowe”. Jest to istotą umowy. Jeżeli programista

spełni wymagania wobec danych wejściowych dla da-

nej metody (lub innej części modułu) to jej twórca infor-

muje i zapewnia go o tym, czego oczekiwać może na

wyjściu. Takimi zależnościami można opleść kolejne

metody, klasy, pakiety a w efekcie całą aplikację.

W praktyce programowanie z wykorzystaniem pro-

jektowania związanego umową sprowadza się do stwo-

JML

JML (ang. Java Modeling Language ) jest formalną me-

todą specyikacji właściwości implementacji bazującą

na idei projektowania związanego umową. Notacja ta

umożliwia szczegółowy opis zachowania klas oraz in-

terfejsów w języku Java. JML nie wymaga od projektan-

tów (programistów) stosowania ściśle określonej meto-

dyki projektowania. Modelowanie zachowania modułów

może być wykonane zarówno przed jak i po ich imple-

mentacji. W praktyce efekt DBC osiąga się poprzez od-

powiednie skomentowanie kodu źródłowego (określenie

warunków, które muszą być spełnione podczas wyko-

nywania programu) oraz zastosowanie narzędzi, które

pozwalają na kompilację klas z automatycznym doda-

niem odpowiednich asercji sprawdzanych podczas wy-

konania, analizę statyczną lub formalną weryikację.

Główną zaletą JML, o czym czytelnik za chwilę

się przekona, jest jego prostota. Zastosowanie narzę-

dzi do formalnej weryikacji kodu w większości przy-

padków wiąże się z opanowaniem odpowiednich tech-

Autor jest doktorantem w Instytucie Informatyki Poli-

techniki Warszawskiej. Pracuje w Wincor Nixdorf.

Kontakt z autorem: pnazimek@gmail.com.

Strona WWW: http://home.elka.pw.edu.pl/~pnazimek/.

www.sdjournal.org Software Developer’s Journal 8/2006

D okumentowanie i testowanie oprogramowania

Java Modeling Language

Listing 1. Interfejs Function

Listing 2. Jedna z metod z interfejsu Function wraz ze

specyikacją w JML

public interface Function {

public Double val ( Double x ) ;

public Double der ( Double x ) ;

public String toString () ;

public String toStringDer () ;

}

/* @ requires x != null;

@ ensures \result != null; */

public /*@ pure @*/ Double val ( Double x ) ;

minację niepotrzebnych asercji i warunków wykonania. Możliwe

jest również tworzenie klas testujących dla narzędzia JUnit .

nik notacji, najczęściej mocno odbiegających od sposobu zapi-

su kodu źródłowego. JML jest bardzo zbliżony do samego ję-

zyka Java dzięki czemu jego opanowanie przez programistę

znającego ten język zajmuje nie więcej niż kilka godzin. Zale-

ta ta sprawia, że JML jest coraz częściej używany jako narzę-

dzie zwiększające niezawodność oprogramowania poprzez

wykluczenie wielu błędów spowodowanych niepoprawnym za-

pisem algorytmu czy sytuacjami wyjątkowymi nieprzewidziany-

mi przez programistę jeszcze na etapie implementacji i wstęp-

nych testów na aplikacji niedziałającej produkcyjnie,. Ponadto

konieczność zastosowania dodatkowych komentarzy skłania

do dokładniejszego przemyślenia (podobnie jak przy progra-

mowaniu ekstremalnym) fragmentów tworzonego kodu źródło-

wego. Następnie opracowana specyikacja może posłużyć do

dodatkowej weryikacji zgodności modelu z implementacją oraz

stworzenia szczegółowej dokumentacji.

Kod źródłowy, opatrzony specyikacją w JML, może posłu-

żyć do automatycznej generacji kodu wynikowego zawierające-

go odpowiednie asercje przed, po i w trakcie wywoływania me-

tod. Oczywiście wpływają one na szybkość działania progra-

mu, ale mogą być wykorzystywane jedynie podczas testowania

modułów. System produkcyjny nie musi ich zawierać. Co wię-

cej, zastosowanie JML, a przez to idei projektowania związane-

go umową, może znacząco uprościć kod źródłowy poprzez eli-

Notacja JML

Używanie JML najlepiej zaprezentować na przykładzie. Bę-

dzie to prosta biblioteka matematyczna, której zadaniem bę-

dzie obliczanie wartości funkcji jednej zmiennej i ich pochod-

nych zarówno w postaci numerycznej jak i symbolicznej. Pod-

stawowy interfejs dla klas tej biblioteki zawiera Listing 1.

Patrząc na przeznaczenie kolejnych metod, nawet bez ich

konkretnych implementacji, można określić warunki jakie wydają

się oczywiste na wejściu do metod obliczających wartość funkcji

i pochodnej. Argument musi być liczbą. Konieczność sprawdza-

nia czy x!=null można przerzucić na implementację metod, ale

takie podejście ma co najmniej trzy wady. Po pierwsze – kom-

plikuje implementację i jest redundantne – zapis if (x!=null)

{ /* ... */ } będzie musiał pojawić się w każdej implementa-

cji tych metod. Po drugie – celem tych metod nie jest sprawdza-

nie poprawności na wejściu, ale obliczenie konkretnych warto-

ści. Po trzecie – co zrobić, jeśli warunek x!=null nie jest spełnio-

ny? Naturalną odpowiedzią wydaje się zgłoszenie wyjątku. Jed-

nak to znów skomplikuje nie tylko implementacje samych metod,

ale również kod je wykorzystujący (obsłużenie wyjątku). A prze-

cież wciąż mamy do czynienia z prostymi metodami obliczający-

mi wartość funkcji i jej pochodnej... Problem ten można roz-

wiązać dopisując odpowiednie warunki początkowe. W JML

ujmuje je się w specjalne komentarze:

/*@

@ requires (* tu warunki w JML *);

@*/

Można również stosować skróconą wersję: //@ requires (* tu wa-

runki w JML *); Warunki są wyrażeniami logicznymi. Listing 2 za-

wiera metodę public Double val(Double x) wraz z odpowiednim

wymaganiem związanym z daną wejściową i wyjściową. Jeżeli

użytkownik tej metody zapewni x różne od null to twórca tej me-

tody zapewnia go, że na wyjściu nie otrzyma on wartości null .

Zapis pure w deklaracji metody informuje, że nie wpływa ona na

składowe klasy. Poza operatorami logicznym znanymi z języka

Java ( == , != , && , || , ! ) w JML zdeiniowano dodatkowo:

l x==>y , y<==x – z x wynika y ,

l x<==>y – x jest spełnione wtedy i tylko wtedy gdy y jest

spełnione,

l x<=!=>y – negacja logicznej wartości wyrażenia x<==>y .

Najważniejsze klauzule, które można użyć w specyikacji:

Rysunek 2. Aplikacja jml w wersji GUI

l \result – określa wartość zwracaną przez metodę,

l \old(X) – określa wartość zmiennej X przed wykonaniem

metody.

Software Developer’s Journal 8/2006

www.sdjournal.org

Programowanie

Java

Listing 3. Fragment implementacji klasy Sum

Warunki będące publicznymi niezmiennikami są weryiko-

wane podczas zakończenia działania konstruktorów obiek-

tów oraz na początku i końcu każdej z wykonywanych me-

tod. Możliwe jest również określenie niezmienników obowią-

zujących wyłącznie w obrębie danej klasy. Określają one naj-

częściej dopuszczalne stany składowych klasy. Dotychczas

w modelu JML wykorzystywaliśmy jedynie argumenty wej-

ściowe opisywanych metod, wywołania samych metod oraz

słowa kluczowe JML. Poza tymi elementami możliwe jest rów-

nież wykorzystanie składowych klas. Dwie składowe zawie-

ra klasa Sum , która reprezentuje sumę dwóch funkcji podanych

przy wywołaniu konstruktora. Fragment jej implementacji zo-

stał przedstawiony na Listingu 3. Aby w JML móc wykorzy-

stać składowe f1 i f2 należy je uczynić publicznymi w specyi-

kacji, co zapisujemy w następujący sposób:

public class Sum implements Function {

private Function f1 ;

private Function f2 ;

public Sum ( Function f1 , Function f2 ) {

this . f1 = f1 ;

this . f2 = f2 ;

}

public Double val ( Double x ) {

return new Double ( f1 . val ( x ) . doubleValue () + f2 . val ( x ) .

doubleValue ()) ;

}

public Double der ( Double x ) {

return new Double ( f1 . der ( x ) . doubleValue () + f2 . der ( x ) .

doubleValue ()) ;

}

private /*@ spec_public @*/ Function f1;

private /*@ spec_public @*/ Function f2;

Zauważmy, że w interfejsie Function nie możemy określić spe-

cyicznych wymagań wobec wartości x . Przykładowo dla funk-

cji ln(x) wartość argumentu musi być większa od zera. Moż-

liwe są dwa rozwiązania tego problemu. Pierwsze polega na

ujęciu tego warunku w klauzuli requires , co wymusi walidację

danych wejściowych na osobie korzystającej z metody. Nale-

ży to oczywiście zrobić już przy jej konkretnej implementacji:

Poza tym zauważmy, że zmienne f1 i f2 nigdy nie powinny

być równe null . Można to oczywiście opisać jako warunek

wywołania konstruktora lub niezmiennik. Najprościej i najczy-

telniej jednak zapisać to wraz z deklaracją:

private /*@ spec_public not_null @*/ Function f1;

private /*@ spec_public not_null @*/ Function f2;

//@ also

//@ requires x.doubleValue() > 0.0 ;

Co jednak zrobić, kiedy warunek, jaki powinien być spełnio-

ny jest niemożliwy do wyrażenia bez rozszerzenia możliwo-

ści specyikacji JML? Nie należy z niego rezygnować. Moż-

na zapisać go w postaci specyikacji informacyjnej. Oczywi-

ście taka specyikacja nie będzie brana pod uwagę przy au-

tomatycznym testowaniu. Posłuży jednak do generowania do-

kumentacji. Przykładowo w interfejsie Function , klauzulę ensu-

res metody val(Double x) można rozszerzyć o:

Słowo kluczowe also oznacza uwzględnienie tego dodatko-

wego warunku oraz wszystkich poprzednich pochodzących

(w tym przypadku) z interfejsu. Drugie rozwiązanie to określe-

nie warunku końcowego w postaci wyjątku. Dla złego argu-

mentu, metoda obliczająca wartość logarytmu zgłosi wyjątek

IllegalArgumentException , co można zapisać jako:

@ ensures \result != null

@ && (* zwracana wartość odpowiada implementowanej wartości

funkcji *); */

/*@ signals (IllegalArgumentException e)

@ ! (x.doubleValue() > 0.0); */

Taki zapis nie oznacza jednak, że nie mogą pojawić się inne sy-

tuacje wyjątkowe. Aby szczegółowo określić wyjątki, jakie mogą

się pojawić należy skorzystać z klauzuli

Listing 4. Fragment utworzonego pliku Constant_JML_

TestData.java

private org . jmlspecs . jmlunit . strategies . StrategyType

vjava_lang_DoubleStrategy =

new org . jmlspecs . jmlunit . strategies .

ImmutableObjectAbstractStrategy () {

protected java . lang . Object [] addData () {

return new java . lang . Double [] {} ;

}

} ;

private org . jmlspecs . jmlunit . strategies . StrategyType

vorg_software20_jmlsample_ConstantStrategy =

new org . jmlspecs . jmlunit . strategies .

NewObjectAbstractStrategy () {

protected Object make ( int n ) {

switch ( n ) { default : break ; }

throw new java . util . NoSuchElementException () ; }

} ;

signals_only: //@ signals_only IllegalArgumentException;

W wyżej opisany sposób można określić wymagania wobec po-

zostałych metod.

Przyjrzyjmy się teraz interfejsowi Function pod kątem nie

tylko warunków wejściowych i wyjściowych ale również tzw.

niezmienników. Jednym z nich może być wymaganie opisu-

jące wartości zwracane przez metody toString() i toString-

Der() . Nie powinny one nigdy zwrócić null ani być wartościa-

mi pustymi:

//@ public invariant toString() != null

//@ && toStringDer() != null

//@ && !toString().equals(“”)

//@ && !toStringDer().equals(“”);

www.sdjournal.org Software Developer’s Journal 8/2006

Programowanie

Java

Do sprawdzania bardziej skomplikowanych warunków (np. gdy

zmienna wejściowa jest tablicą) mogą posłużyć liczne zaimple-

mentowane w JML kwantyikatory. Do podstawowych należą:

JML-Scripts (w katalogu wskazanym przez JMLDIR ) konieczne

jest dodatkowo określenie:

l \forall – dla wszystkich,

l \exists – istnieje,

l \min , \max – wartość minimalna, maksymalna.

l INSTALLTYPE – w zależności od typu instalacji: cygwin (je-

żeli korzystamy z JML w środowisku Cygwin ) lub unix (dla

platform typu unix lub linux )

l INSTALLDIR – docelowe położenie skryptów uruchamiają-

cych narzędzia JML oraz stron manuali (np. /usr/local )

Przykładowo, aby wyrazić konieczność dostarczenia na wej-

ściu do metody posortowanej tablicy tab z elementami typu

int można zastosować warunek:

W systemie Microsoft Windows należy zatroszczyć się o to, aby

dostęp do skryptów uruchamiających narzędzia JML (znajdują się

w ścieżce JMLDIR/bin ) był możliwy przez zmienną środowiskową

PATH . Aktualna wersja JML została w pełni przetestowana z ma-

szyną wirtualną Java w wersji 1.4.2 i jest ona zalecana do użycia.

\@ requires (\forall int k;

\@ 0 < k && k < tab.length;

\@ tab[k-1] <= tab[k]);

Narzędzia JML

Na Rysunku 1 przedstawiono okno aplikacji jml-launcher , która

pozwala na uruchamianie narzędzi JML w wygodnej wersji gra-

icznej. Przy okazji warto zwrócić uwagę na logo projektu – do-

kładnie zwymiarowany kubek z kawą. Kolejne narzędzia to:

Możliwe jest również rozszerzanie modelu JML poprzez im-

plementację statycznych metod opisujących odpowiednie wa-

runki. Kilkanaście takich klas zostało już stworzonych. Przy-

kładem może być metoda JMLDouble.approximatelyEqualTo-

(wartosc1, wartosc2, epsilon) , która sprawdza warunek |war-

tosc1 - wartosc2|<=epsilon dla zmiennych typu double .

l JML Type Checker – umożliwia weryikację statyczną,

l JML Runtime Assertion Checker Compiler – przeznaczony

kompilowania kodu z przeznaczeniem do weryikacji dyna-

micznej,

l JML Documentation – tworzenie dokumentacji modelu,

l JML Skeleton Spec Generator – generowanie namiastek

specyikacji,

l JML / JUnit Test Oracle Generator – automatyczne two-

rzenie testów dla JUnit na podstawie specyikacji JML.

Przygotowanie środowiska JML

Do pracy potrzebny będzie również JUnit umożliwiający automa-

tyczne testowanie klas na podstawie stworzonych scenariuszy

i szczegółowo opisany we wcześniejszych wydaniach magazy-

nu Software Developer’s Journal . Oba pakiety udostępniane są

w formie archiwów. Do ich działania niezbędna jest zainstalowa-

na i skonigurowana wirtualna maszyna języka Java. Po rozpako-

waniu archiwów zawierających JML i JUnit należy ustawić nastę-

pujące zmienne środowiskowe:

Każde z tych narzędzi można używać w wersji z interfejsem

graicznym lub bezpośrednio z linii komend.

l JMLDIR – wskazuje miejsce, gdzie rozpakowano archiwum

z pakietem JML

l JUNITDIR – wskazuje miejsce, gdzie rozpakowano archi-

wum z pakietem JUnit

l JDKTOOLS – wskazuje położenie pliku tools.jar w katalogu

gdzie zainstalowano Javę (np.: /opt/sun-jdk-1.4.2.10/lib/

tools.jar )

Weryikacja statyczna

Aplikacja jml (w wersji GUI jml-gui ) pozwala na statyczną

weryikację kodu tj. bez jego kompilacji, tak jak to się dzie-

je w przypadku weryikacji dynamicznej. Sprawdzenie obej-

muje między innymi poprawność formalną specyikacji JML,

zgodność typów oraz odwołań do metod. Na Rysunku 2 po-

kazano aplikację jml-gui z zaimportowanymi plikami do we-

ryikacji. Każdy wykryty błąd jest szczegółowo raportowany.

Ponadto zmienną CLASSPATH należy rozszerzyć o wpis określa-

jący katalogi JMLDIR oraz JMLDIR/specs . Przed rozpoczęciem

instalacji w środowisku Cygwin lub Linux/Unix , poza wyżej wy-

mienionymi zmiennymi środowiskowymi, w pliku bin/Install-

Weryikacja dynamiczna

Weryikacja dynamiczna polega na sprawdzeniu czy wyma-

gane warunki spełnione są podczas wykonania programu.

Wszystkie adnotacje w JML zamieniane są wtedy na odpo-

Literatura

Wszystkie wymienione niżej artykuły można pobrać ze strony pro-

jektu JML.

Listing 5. Plik Function.reines-spec

l Yoonsik Cheon i Gary T. Leavens. Design by Contract with

JML . April 2005.

l Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael Ernst,

Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll.

An Overview of JML Tools and Applications .

l Yoonsik Cheon i Gary T. Leavens. The JML and JUnit Way of

Unit Testing and its Implementation .

l Yoonsik Cheon, Myoung Yee Kim i Ashaveena Perumandla.

A Complete Automation of Unit Testing for Java Programs .

package org.software20.jmlsample;

//@ reine "Function.java";

public interface Function {

// INTERFACE SPECIFICATIONS METHODS

Double val ( Double x ) ;

Double der ( Double x ) ;

String toString () ;

String toStringDer () ;

}

www.sdjournal.org Software Developer’s Journal 8/2006

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika: