Java Modeling Language

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 надає наступні ключові слова:

requires — описує передумови.
ensures — описує післяумови.
signals — описує післяумову для випадку, коли виникло задане виключення у методі.
signals_only — визначає, які виключення можуть бути кинуті, коли виконується задана передумова.
assignable — визначає, яким поля може бути присвоєне значення в наступному методі.
pure — оголошує метод який не продукує побічних ефектів.
invariant — визначає інваріантну нерухомість класу.
loop_invariant — визначає інваріант циклу.
also — поєднує декілька описів, а також може вказувати на те, що метод успадковує опис від свого супертипу.
assert — визначає всюди істинне твердження JML.
spec_public — робить захищену (protected) або приватну (private) змінну доступною для потреб специфікації.
\result — задає ім'я для результату.
\old(<expression>) — модифікатор для звернення до значення < expression > на момент входу в метод.
(\forall <decl>; <range-exp>; <body-exp>) — квантор «для будь-якого».
(\exists <decl>; <range-exp>; <body-exp>) — квантор існування.
a ==> b — з a слідує b.
a <== b — a наслідується з b.
a <==> b — a тоді і тільки тоді коли b, а також стандартний синтаксис Java для логічного І, АБО, і НІ. JML анотації також мають доступ до об'єктів Java, методів об'єктів і операторів, які в рамках методу анотуються і мають відповідну видимість. Така сукупність дозволяє описувати формальні специфікації властивостей класів, полів і методів. Наприклад, приклад простого банківського класу:

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 ред.

JML це формальна мова специфікації з прив'язкою до Java. Таким чином, її основне використання — формальний опис поведінки модулів Java-застосунків. Так як JML — це поведінкова мова специфікації інтерфейсу, яка описує спосіб використання окремих модулів за межами Java-застосунків — вона не призначений для опису поведінки всієї програми загалом. Так питання «Для чого JML краще підходить?» дійсно зводиться до наступного питання: що хорошого дає формальна специфікація програмних модулів Java? Дві головні переваги використанні JML:

точний, однозначний опис поведінки програмних модулів на Java (тобто, класів і інтерфейсів), і документування коду Java,
можливість інструментів підтримки [13].

Хоча ми хотіли б інструменти, які допоможуть з паралельним програмуванням програм Java, поточна версія JML фокусується на послідовному поведінці Java коду. У той час як робота триває з розширення JML для підтримки паралелізму [14], поточна версія JML не має функції, яка допоможе визначити, як Java потоки взаємодіють один з одним. З точки зору детальної проектної документації, специфікація JML може надати зовсім формальний опис інтерфейсу і його послідовної поведінки. Мета JML — зробити запис байдужим до точних методів програмування. Можна використовувати JML або для кодування або документації готового коду. Причини для офіційної документації інтерфейсів і їх поведінки, використовуючи JML, включають в себе наступне.

Можна відправити об'єктний код бібліотеки класів клієнту, відправляти специфікації Jml, але не вихідний код. Клієнти отримають документацію, яка є точною, однозначною, але не надмірно конкретною. Клієнти не матимуть код, захисту прав власності. Крім того, клієнти не будуть покладатися на деталі реалізації бібліотеки, полегшуючи процес поліпшення коду в майбутніх версіях.
Можна використовувати специфікацію JML як допомогу для ретельного обміркування правильності коду, або навіть для формальної верифікації [15].
Технічні характеристики JML можуть використовуватись декількома інструментами, які можуть допомогти налагодити і поліпшити код [16].

Джерела ред.

John V. Guttag and James J. Horning with S.J. Garland, K.D. Jones, A. Modet and J.M. Wing. Larch: Languages and Tools for Formal Specification (Springer-Verlag, NY, 1993).
John V. Guttag and James J. Horning and Jeannette M. Wing. The Larch Family of Specification Languages. IEEE Software, 2(5):24-36, September 1985.
David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19–31, January 1995.
Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, N.Y., 1992.
Jeannette M. Wing. A Specifier's Introduction to Formal Methods. Computer, 23(9):8-24, September 1990.
Leslie Lamport. A Simple Approach to Specifying Concurrent Systems. CACM, 32(1):32-45, January 1989.
Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99 — Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Proceedings, volume 1709 of Lecture Notes in Computer Science, pages 1087–1106. Springer-Verlag, 1999.
K. Rustan M. Leino. Towards Reliable Modular Programs. PhD thesis, California Institute of Technology, January 1995
Alex Borgida, John Mylopoulos, and Raymond Reiter. On the Frame Problem in Procedure Specifications. IEEE Transactions on Software Engineering, 21(10):785-798, October 1995
Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, and Stephen Edwards. Model Variables: Cleanly Supporting Abstraction in Design By Contract. Software--Practice and Experience, 35(6):583-599, May 2005
I. Hayes (ed.), Specification Case Studies, second edition (Prentice-Hall, Englewood Cliffs, N.J., 1990)
Alan Wills. Specification in Fresco. In Susan Stepney and Rosalind Barden and David Cooper (eds.), Object Orientation in Z, chapter 11, pages 127–135. Springer-Verlag, Workshops in Computing Series, Cambridge CB2 1LQ, UK, 1992
Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. Dept. of Computer Science, University of Nijmegen, TR NIII-R0309, 2003
Edwin Rodriguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby. Extending JML for Modular Specification and Verification of Multi-Threaded Programs. In Andrew P. Black (ed.), ECOOP 2005
Marieke Huisman. Reasoning about JAVA programs in higher order logic with PVS and Isabelle. IPA dissertation series, 2001-03. Ph.D. dissertation, University of Nijmegen, 2001
Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In ECOOP 2002
Clyde Ruby and Gary T. Leavens. Safely Creating Correct Subclasses without Seeing Superclass Code. In OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota. (ACM SIGPLAN Notices, 35(10):208-228, October, 2000.)
Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. ACM SIGSOFT Software Engineering Notes, 31(3):1-38, March 2006.
Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In ECOOP 2002
Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. Dept. of Computer Science, University of Nijmegen, TR NIII-R0309, 2003.

Ланки ред.

Java Modeling Language (англ.)