Yazan  : Şadi Evren ŞEKER

JML ingilizce Java modelling language kelimelerinin baş harflerinden oluşan bir kısaltmadır. Basitçe bir java kaynak koduna eklenen ilave satırlar ile progam doğruluğunu (program correctness) sağlamayı amaçlar (program verification).

İlave olarak eklenecek satırlar java kodunun içerisine yorum satırı gibi ilave edilir. Normal java yorum satırlarından tek farkı ilave olarak konulan @ işaretidir.

Örneğin

//@ örnek jml satırı

veya

/*@ örnek
çoklu jml
satırı @*/

şeklinde java koduna ilave edilebilirler.

Aslında bütün jml komutlarını basit üç grupta toplamak mümkündür:

  1. Önkoşullar (preconditions)
  2. Sonkoşullar (postconditions)
  3. Değişmezler (invariants)

Yukarıdaki bu üç grubtan ilk ikisi hoare mantığındaki ön ve son koşullara benzetilebilir. Üçüncü grup ise döngülere özgü kullanılan bir koşuldur. Bu gruplardaki komutları ve kullanımlarını aşağıdaki örneklerden inceleyelim:

static void arraycopy (int[] src, int srcPos,int[] dest, int destPos,int len);

Örnek olarak yukarıdaki dizi (array) kopyalama fonksiyonunu ele alalım. Burada amaç, src dizisinden dest dizisine derin kopyalama yapmaktır. (deep copy). Ancak bu satırda yaşanabilecek bazı programlar aşağıdaki şekildedir:

  • src dizisi null olabilir
  • dest dizisi null olabilir
  • src dizisinin izin verilen eleman sayısının dışına programcı tarafından çıkılabilir (örneğin 10 elemanlı bir dizinin 10. elemanına erişilebilir (java terminolojisi olarak arrayindexoutofboundsexception olabilir))
  • dest dizisinin izin verilen eleman sayısının dışına programcı tarafından çıkılabilir.

Bu yazı şadi evren şeker tarafından yazılmış ve bilgisayarkavramlari.com sitesinde yayınlanmıştır. Bu içeriğin kopyalanması veya farklı bir sitede yayınlanması hırsızlıktır ve telif hakları yasası gereği suçtur.

Yukarıdaki bu olası problemleri çözmek için fonksiyonu yazarken başına ilave olarak bu requires komutu ile ön koşullarımızı ekliyoruz.

/*@ requires src != null && dest != null &&
0 <= srcPos && srcPos + len < src.length &&
0 <= destPos && srcPos + len < dest.length;
@*/
static void arraycopy (int[] src, int srcPos,int[] dest, int destPos,int len);

Yukarıdaki yeni kodda ilave olarak src ve dest’in null olamayacakları ve kopyalama sırasında kullanılan indis değişkeni olan srcPos’un 0 ile src.length ve dest.length arasında olacağı belirtilmiştir.

Yukarıdaki ön koşula ilave olarak diğer bir isteğimiz fonksiyon çalıştıktan sonra src ile dest dizilerinin elemanlarının birebir aynı olmalarıdır. Bu son koşulu (postcondition) kontrol etmek için ilave bir jml satırı daha eklememiz gerekir:

/*@ requires src != null && dest != null &&
0 <= srcPos && srcPos + len < src.length &&
0 <= destPos && srcPos + len < dest.length;
ensures (forall int i; 0 <= i && i < len;dest[dstPos+i] == src[srcPos+i] )
@*/
static void arraycopy (int[] src, int srcPos,int[] dest, int destPos,int len);

Yukarıdaki yeni jml satırı olan ensures ile son koşul kontrolü yapılıyor.  Burada yeni kullanılan forall döngüsü sayesinde 0’dan len değişkenine kadar olan değerler için (döngü değişkeni i olarak) bütün dizi içeriği karşılaştırılıyor ve ancak aynıysa son koşul sağlanmış oluyor.

Bir cevap yazın

E-posta hesabınız yayımlanmayacak. Gerekli alanlar * ile işaretlenmişlerdir