Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

Язык моделирования Java ( JML ) - это язык спецификации для программ Java , использующий предварительные и постусловия и инварианты стиля Хоара , который следует парадигме проектирования по контракту . Спецификации записываются в виде комментариев Java-аннотаций к исходным файлам, которые, следовательно, могут быть скомпилированы с помощью любого компилятора Java .

Различные инструменты проверки, такие как средство проверки утверждений во время выполнения и средство расширенной статической проверки ( ESC / Java ), помогают в разработке.

Обзор [ править ]

JML - это язык спецификации поведенческого интерфейса для модулей Java. JML предоставляет семантику для формального описания поведения модуля Java, предотвращая неоднозначность намерений разработчиков модуля. JML унаследовал идеи от Эйфеля , Ларча и исчисления уточнений с целью обеспечения строгой формальной семантики, при этом оставаясь доступным для любого Java-программиста. Доступны различные инструменты, использующие поведенческие спецификации JML. Поскольку спецификации могут быть записаны как аннотации в программных файлах Java или сохранены в отдельных файлах спецификаций, модули Java со спецификациями JML могут быть скомпилированы без изменений с помощью любого компилятора Java.

Синтаксис [ править ]

Спецификации JML добавляются в код Java в виде аннотаций в комментариях. Комментарии Java интерпретируются как аннотации JML, если они начинаются со знака @. То есть комментарии формы

// @ <спецификация JML>

или же

/ * @ <Спецификация JML> @ * /

Базовый синтаксис JML включает следующие ключевые слова

requires
Определяет предварительное условие для следующего метода .
ensures
Определяет постусловие для следующего метода.
signals
Определяет постусловие, когда данное исключение выбрасывается последующим методом.
signals_only
Определяет, какие исключения могут возникать при выполнении данного предусловия.
assignable
Определяет, какие поля могут быть присвоены с помощью следующего метода.
pure
Объявляет метод свободным от побочных эффектов (например, assignable \nothingно может также вызывать исключения). Кроме того, чистый метод должен всегда либо завершаться нормально, либо вызывать исключение.
invariant
Определяет инвариантное свойство класса .
loop_invariant
Определяет инвариант цикла для цикла.
also
Объединяет случаи спецификации, а также может объявить, что метод наследует спецификации от своих супертипов.
assert
Определяет утверждение JML .
spec_public
Объявляет защищенную или частную переменную общедоступной для целей спецификации.

Базовый JML также предоставляет следующие выражения

\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 для логических and, or и not. Аннотации JML также имеют доступ к объектам Java, методам объектов и операторам, которые находятся в пределах области действия аннотируемого метода и имеют соответствующую видимость. Они объединены, чтобы предоставить формальные спецификации свойств классов, полей и методов. Например, аннотированный пример простого банковского класса может выглядеть так:

public  class  BankingExample {  публичный  статический  финал  int  MAX_BALANCE  =  1000 ;  private  / * @ spec_public @ * /  int  balance ;  private  / * @ spec_public @ * /  логическое  isLocked  =  false ;   // @ публичный инвариантный баланс> = 0 && balance <= MAX_BALANCE;  // @ назначаемый баланс;  // @ обеспечивает баланс == 0;  public  BankingExample ()  {  это . баланс  =  0 ;  }  // @ требуется 0 <сумма && сумма + баланс <MAX_BALANCE;  // @ назначаемый баланс;  // @ обеспечивает баланс == \ old (balance) + amount;  общественный  недействительный  кредит ( окончательная  сумма int  ) { this . баланс + = сумма ; }       // @ требуется 0 <сумма && сумма <= баланс;  // @ назначаемый баланс;  // @ обеспечивает баланс == \ old (balance) - amount;  public  void  debit ( final  int  amount )  {  this . баланс  - =  сумма ;  }  // @ гарантирует isLocked == true;  public  void  lockAccount ()  {  this . isLocked  =  true ;  }  // @ требуется! isLocked;  // @ обеспечивает \ result == баланс;  // @ также  // @ требуется isLocked;  // @ signal_only BankingException;  public  / * @ pure @ * /  int  getBalance ()  выдает  исключение BankingException  {  if  ( ! this . isLocked )  {  вернуть  это . баланс ;  }  else  {  выбросить  новое  исключение BankingException ();  }  } }

Полная документация по синтаксису JML доступна в Справочном руководстве JML .

Поддержка инструмента [ править ]

Разнообразные инструменты предоставляют функциональные возможности на основе аннотаций JML. Инструменты JML штата Айова предоставляют компилятор проверки утверждений, jmlcкоторый преобразует аннотации JML в утверждения среды выполнения, генератор документации, jmldocкоторый создает документацию Javadoc, дополненную дополнительной информацией из аннотаций JML, и генератор модульных тестов, jmlunitкоторый генерирует тестовый код JUnit из аннотаций JML.

Независимые группы работают над инструментами, использующими аннотации JML. К ним относятся:

  • ESC / Java2 [1] , расширенная статическая проверка, которая использует аннотации JML для выполнения более строгой статической проверки, чем это возможно в противном случае.
  • OpenJML объявляет себя преемником ESC / Java2.
  • Дайкон , динамический инвариантный генератор.
  • KeY , который предоставляет средство доказательства теорем с открытым исходным кодом с интерфейсом JML и подключаемый модуль Eclipse ( редактирование JML ) с поддержкой подсветки синтаксиса JML.
  • Krakatoa , инструмент статической проверки, основанный на платформе проверки Why и использующий помощник проверки Coq .
  • JMLEclipse , плагин для интегрированной среды разработки Eclipse с поддержкой синтаксиса JML и интерфейсом для различных инструментов, использующих аннотации JML.
  • Sireum / Kiasan , статический анализатор на основе символьного исполнения, поддерживающий JML в качестве языка контрактов.
  • JMLUnit , инструмент для создания файлов для запуска тестов JUnit на файлах Java с аннотациями JML.
  • TACO , инструмент анализа программ с открытым исходным кодом, который статически проверяет соответствие программы Java ее спецификации языка моделирования Java.
  • Верификатор VerCors

Ссылки [ править ]

  • Гэри Т. Ливенс и Юнсик Чеон. Дизайн по контракту с JML ; Черновик учебника.
  • Гэри Т. Ливенс , Альберт Л. Бейкер и Клайд Руби. JML: обозначение для детального проектирования ; в Хаим Килов, Бернхард Румпе и Ян Симмондс (редакторы), Поведенческие спецификации предприятий и систем , Kluwer, 1999, глава 12, страницы 175–188.
  • Гэри Т. Ливенс , Эрик Полл, Кертис Клифтон, Юнсик Чеон, Клайд Руби, Дэвид Кок, Питер Мюллер, Джозеф Кинири, Патрис Чалин и Дэниел М. Циммерман. Справочное руководство JML (ПРОЕКТ), сентябрь 2009 г. HTML
  • Марике Хейсман , Вольфганг Арендт, Даниэль Брунс и Мартин Хентшель. Формальная спецификация с JML . 2014. скачать (CC-BY-NC-ND)

Внешние ссылки [ править ]

  • Веб-сайт JML