The Java Modeling Language (JML) — мова, яка використовується для опису функціональної поведінки класів і методів Java. Опис поведінки виражається у вигляді структурованих Java-коментарів чи анотацій Java, що використовують Java, як логічні вирази. Різні інструменти можуть прочитати інформацію JML і виконати статичну перевірку, перевірку виконання, генерацію тестів, відображення документації або інших корисних завдань.
JML — поведінкова мова специфікації інтерфейсу (BISL), яка ґрунтується на підході Larch [1] [2]. Її стиль специфікації можна назвати модель-орієнтованим [5], який одночасно визначає як інтерфейс методу або абстрактного типу даних так і його поведінку [6]. Зокрема JML ґрунтується на роботу, виконаній Левенсом(Leavens) та іншими над Larch / C ++ [7]. Дизайну JML зазнав значного впливу робіт Лейно і його співробітників [8]. JML знаходиться під постійним впливом роботи у галузі формальній специфікації і верифікації.
Інтерфейс методу або типу даних(класу у Java) — інформація, що використовується іншими частинами програми. У випадку JML, це Java-синтаксис і інформація про типи, необхідна для виклику методу або використання поля чи типу(класу). Для методу інтерфейс включає в себе таку інформацію, як ім'я методу, його модифікатори (у тому числі його видимість і чи є воно константним (final)) його кількість аргументів, тип результату, які виключення він може генерувати, і так далі. Для поля, інтерфейс включає в себе його назву і тип, і модифікатори. Для типу, інтерфейс включає в себе назву, його модифікатори, пакет, до якого він належить, незалежно від того це клас чи інтерфейс, його батьківські класи і інтерфейси(описи) полів і методів які він оголошує або успадковує. JML визначає всю інформацію інтерфейсу(опису), використовуючи синтаксис Java.
Поведінка методу або типу описує набір змін станів, що він може виконувати. Поведінка методу визначається: набором станів, у яких виклик методу дозволений, набір випадків у яких методу дозволено виконувати присвоєння (і, отже, змінити), і відношеннями між станом у момент виклику та станом в якому він виконується нормально, генерує виключення або для яких він не може закінчитися. Стани, для яких визначено метод формально описується логічними твердженнями(assertioni), які називається передумовою методу. Допустимі відносини між цими станами та станами, які можуть виникнути в результаті успішного виклику формально описуються іншими логічними твердженнями — післяумови методу. Так само відносини між цими попередніми станами і станами, які можуть виникнути в результаті виникнення виключення описані винятковим післяумовами (exceptional postconditions) методу. Стани, для яких метод не повинен повертати значення описуються розбіжними(divergence) умовами; Однак, явна задання таких умов використовується в JML дуже рідко.
Поведінка абстрактного типу даних (АТД), який реалізується за допомогою класів Java, визначається описом набору абстрактних полів для об'єктів і, описом поведінки методів. Абстрактні поля для об'єкта, можуть бути описані або за допомогою моделі JML та за допомогою примарних(ghost) полів, які використовуються тільки специфікацією, або вказавши для полів реалізації анотації spec_public або spec_protected. Такі анотації дозволяють специфікатору з допомогою JML змоделювати об'єкт у вигляді колекції абстрактних полів об'єкту, подібно до таких мов як Z [11] або Fresco [12].
Характеристики JML додаються до Java коду у вигляді анотацій в коментарях. Java коментарі інтерпретуються як Jml анотації, коли вони починають зі знака @. Тобто, коментарі вигляду //@ <JML specification> або /*@ <JML specification> @*/
Основний синтаксис JML надає наступні ключові слова:
public class BankingExample{ public static final int MAX_BALANCE = 1000; private /*@ spec_public @*/ int balance; private /*@ spec_public @*/ boolean isLocked = false; //@ public invariant balance >= 0 && balance <= MAX_BALANCE; //@ assignable balance; //@ ensures balance == 0; public BankingExample(){ this.balance = 0; } //@ requires 0 < amount && amount + balance < MAX_BALANCE; //@ assignable balance; //@ ensures balance == \old(balance) + amount; public void credit(final int amount) { this.balance += amount; } //@ requires 0 < amount && amount <= balance; //@ assignable balance; //@ ensures balance == \old(balance) - amount; public void debit(final int amount){ this.balance -= amount; } //@ ensures isLocked == true; public void lockAccount(){ this.isLocked = true; } //@ requires !isLocked; //@ ensures \result == balance; //@ also //@ requires isLocked; //@ signals_only BankingException; public /*@ pure @*/ int getBalance() throws BankingException{ if (!this.isLocked){ return this.balance; } else{ throw new BankingException(); } } }
JML це формальна мова специфікації з прив'язкою до Java. Таким чином, її основне використання — формальний опис поведінки модулів Java-застосунків. Так як JML — це поведінкова мова специфікації інтерфейсу, яка описує спосіб використання окремих модулів за межами Java-застосунків — вона не призначений для опису поведінки всієї програми загалом. Так питання «Для чого JML краще підходить?» дійсно зводиться до наступного питання: що хорошого дає формальна специфікація програмних модулів Java? Дві головні переваги використанні JML:
Хоча ми хотіли б інструменти, які допоможуть з паралельним програмуванням програм Java, поточна версія JML фокусується на послідовному поведінці Java коду. У той час як робота триває з розширення JML для підтримки паралелізму [14], поточна версія JML не має функції, яка допоможе визначити, як Java потоки взаємодіють один з одним. З точки зору детальної проектної документації, специфікація JML може надати зовсім формальний опис інтерфейсу і його послідовної поведінки. Мета JML — зробити запис байдужим до точних методів програмування. Можна використовувати JML або для кодування або документації готового коду. Причини для офіційної документації інтерфейсів і їх поведінки, використовуючи JML, включають в себе наступне.