Java Modelling Language (JML)


Java Modeling Language (JML) adalah bahasa spesifikasi formal untuk program yang berbasis Java. Paradigma dari JML sama dengan DBC, yaitu terdiri dari precondition, postcondition dan invariant. Dalam pengspesifikasiannya, JML menambahkan anotasi-anotasi ke dalam file java atau disimpan dalam file spesifikasi terpisah. User dapat dengan bebas menentukan kapan menggunakan JML. User dapat menggunakan JML sebelum coding atau sebagai dokumentasi setelah menyelesaikan coding.

Dalam pengimplementasiannya, JML ditulis sebagai komentar dalam program java, sehingga dalam pengkompilasiannya tidak diperlukan perubahan. Jml diawali dengan tanda @.Contoh penulisannya adalah sebagai berikut :

//@ <JML Spesification>

atau

/*@ <JML Spesification> @*/

Tanda @ harus tepat berada di sebelah kanan dari karakter pertama komentar. Komentar yang diawali dengan // @ akan diabaikan oleh JML, sama halnya dengan /* @, seharusnya /*@. Tools tidak memberikan peringatan jika terdapat kesalahan penulisan. Jika terdapat kesalahan seperti itu, tools tidak akan menganggapnya sebagai notasi JML. JML menggunakan beberapa klausa, berikut adalah contoh klausa atau sintaks dasar dalam JML :

requires

mendefinisikan precondition untuk suatu method

ensures

mendefinisikan postcondition untuk suatu method

invariant

mendefinisikan deklarasi invariant

assignable

mendifinisikan field-field yang dapat di-assign oleh method

Batasan utama pada JML adalah ekspresi yang digunakan dalam JML assertion adalah ekspresi yang tidak mempunyai efek samping [9]. Ekspresi Java yang bersifat assignment (=, +=, etc), penambahan (++) dan pengurangan (–) tidak diperbolehkan. Dengan kata lain hanya metode yang bersifat pure yang dapat dipanggil dalam assertion. Suatu method disebut pure jika method tersebut tidak mempunyai efek samping. Beberapa sumber menyebutnya method “query”, karena dapat digunakan untuk mengembalikan status dari sebuah objek tanpa mengubahnya.

Deskripsi Informal & Formal

Langkah pertama dalam menulis contract adalah dengan menyusun komentar pada program yang menjelaskan metode sebagai contract. Artinya, developer harus menyusun komentar tentang behavior dari method kedalam assertion. JML mendukung hal ini dengan tanpa mengharuskannya ditulis dalam bentuk formal (bahasa Java), yaitu dengan menuliskannya dalam deskripsi informal.

Deskripsi informal adalah deskripsi contract (precondition, postcondition dan invariant) yang masih memakai bahasa sehari-hari. Deskripsi informal mudah digunakan dalam membuat dokumentasi dan dapat berguna jika tidak adanya waktu untuk membuat deskripsi formal dari program. Namun, deskripsi informal tidak dapat di-compile oleh JML compiler, sehingga tidak dapat dapat dicek pada saat eksekusi (runtime). Oleh karena itu pembuatan deskripsi informal merupakan tahap optional. Contoh dari penggunaan deskripsi infornal adalah :

/*@ invariant (* length of no_ktp is 13 && gender is male or female *)

@ requires (* input data of id,no_ktp,nama,alamat,telp,gender!=null *)

@ ensures (* member data has been inserted and the value of them

@ are equal to input data*)

@*/

Deskripsi formal adalah deksripsi yang telah menggunakan ekspresi seperti Java, sehingga dapat di-compile dan dieksekusi menggunakan tools. Dalam requires mendefinisikan precondition untuk suatu method ensures mendefinisikan postcondition untuk suatu method penggunaannya, deskripsi formal dapat dikombinasikan dengan deskripsi informal.

JML Tools

Dalam situs resmi JML http://www.jmlspecs.org disebutkan bahwa, “Many tools, One Language”, yang berarti bahwa terdapat banyak tools yang tersedia untuk JML. Inti proses dari keseluruhan tools yang ada adalah parsing dan typechecking. Kedua proses ini akan menangkap adanya kesalahan penulisan (typos), type incompatibilities, penggunaan method/atribut yang tidak ada, dll.

JML compiler (jmlc) sama seperti java compiler seperti javac, yaitu dengan menghasilkan kode-kode byte yang berasal dari file sumber. Perbedaannya terletak pada pengecekkan assertion yang dimasukkan ke dalam kode-kode byte. Jmlc mengecek JML assertion yang terdiri dari precondition, postcondition dan invariant. Penggunaan jmlc pun sama dengan penggunaan java compiler. Sama seperti halnya javac, jmlc menghasilkan bytecode yang nantinya akan dipakai oleh jmlrac (JML Runtime Assertion Checker).

Jmlrac adalah tools yang akan mengecek apakah pada saat running program sesuai dengan spesifikasi kode yang telah dituliskan dalam program. Sebelum memakai jmlrac, diharuskan menggunakan jmlc terlebih dahulu. Namun, JML(versi 5.6) tidak dapat menangani program java yang memakai user interface, khususnya yang berbasis grafik (swing, awt, vector,dll).

http://www.ittelkom.ac.id/library/index.php?view=article&catid=20%3Ainformatika&id=579%3Ajava-modelling-language-jml&option=com_content&Itemid=15

Post a comment or leave a trackback: Trackback URL.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: