Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

The Java Modeling Language JML мова яка використовується для опису функціональної поведінки класів і методів Java Опис п

Java Modeling Language

Java Modeling Language

The Java Modeling Language (JML) — мова, яка використовується для опису функціональної поведінки класів і методів Java. Опис поведінки виражається у вигляді структурованих Java-коментарів чи анотацій Java, що використовують Java, як логічні вирази. Різні інструменти можуть прочитати інформацію JML і виконати статичну перевірку, перевірку виконання, генерацію тестів, відображення документації або інших корисних завдань.


Поведінкові характеристики інтерфейсу

JML — поведінкова мова специфікації інтерфейсу (BISL), яка ґрунтується на підході Larch [1] [2]. Її стиль специфікації можна назвати модель-орієнтованим [5], який одночасно визначає як інтерфейс методу або абстрактного типу даних так і його поведінку [6]. Зокрема JML ґрунтується на роботу, виконаній Левенсом(Leavens) та іншими над Larch / [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].


Джерела

  1. 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).
  2. 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.
  3. David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19–31, January 1995.
  4. Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, N.Y., 1992.
  5. Jeannette M. Wing. A Specifier's Introduction to Formal Methods. Computer, 23(9):8-24, September 1990.
  6. Leslie Lamport. A Simple Approach to Specifying Concurrent Systems. CACM, 32(1):32-45, January 1989.
  7. 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.
  8. K. Rustan M. Leino. Towards Reliable Modular Programs. PhD thesis, California Institute of Technology, January 1995
  9. 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
  10. 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
  11. I. Hayes (ed.), Specification Case Studies, second edition (Prentice-Hall, Englewood Cliffs, N.J., 1990)
  12. 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
  13. 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
  14. 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
  15. 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
  16. Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In ECOOP 2002
  17. 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.)
  18. 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.
  19. Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In ECOOP 2002
  20. 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 (англ.)

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

The Java Modeling Language JML mova yaka vikoristovuyetsya dlya opisu funkcionalnoyi povedinki klasiv i metodiv Java Opis povedinki virazhayetsya u viglyadi strukturovanih Java komentariv chi anotacij Java sho vikoristovuyut Java yak logichni virazi Rizni instrumenti mozhut prochitati informaciyu JML i vikonati statichnu perevirku perevirku vikonannya generaciyu testiv vidobrazhennya dokumentaciyi abo inshih korisnih zavdan Povedinkovi harakteristiki interfejsuJML povedinkova mova specifikaciyi interfejsu BISL yaka gruntuyetsya na pidhodi Larch 1 2 Yiyi stil specifikaciyi mozhna nazvati model oriyentovanim 5 yakij odnochasno viznachaye yak interfejs metodu abo abstraktnogo tipu danih tak i jogo povedinku 6 Zokrema JML gruntuyetsya na robotu vikonanij Levensom Leavens ta inshimi nad Larch C 7 Dizajnu JML zaznav znachnogo vplivu robit Lejno i jogo spivrobitnikiv 8 JML znahoditsya pid postijnim vplivom roboti u galuzi formalnij specifikaciyi i verifikaciyi Interfejs metodu abo tipu danih klasu u Java informaciya sho vikoristovuyetsya inshimi chastinami programi U vipadku JML ce Java sintaksis i informaciya pro tipi neobhidna dlya vikliku metodu abo vikoristannya polya chi tipu klasu Dlya metodu interfejs vklyuchaye v sebe taku informaciyu yak im ya metodu jogo modifikatori u tomu chisli jogo vidimist i chi ye vono konstantnim final jogo kilkist argumentiv tip rezultatu yaki viklyuchennya vin mozhe generuvati i tak dali Dlya polya interfejs vklyuchaye v sebe jogo nazvu i tip i modifikatori Dlya tipu interfejs vklyuchaye v sebe nazvu jogo modifikatori paket do yakogo vin nalezhit nezalezhno vid togo ce klas chi interfejs jogo batkivski klasi i interfejsi opisi poliv i metodiv yaki vin ogoloshuye abo uspadkovuye JML viznachaye vsyu informaciyu interfejsu opisu vikoristovuyuchi sintaksis Java Povedinka metodu abo tipu opisuye nabir zmin staniv sho vin mozhe vikonuvati Povedinka metodu viznachayetsya naborom staniv u yakih viklik metodu dozvolenij nabir vipadkiv u yakih metodu dozvoleno vikonuvati prisvoyennya i otzhe zminiti i vidnoshennyami mizh stanom u moment vikliku ta stanom v yakomu vin vikonuyetsya normalno generuye viklyuchennya abo dlya yakih vin ne mozhe zakinchitisya Stani dlya yakih viznacheno metod formalno opisuyetsya logichnimi tverdzhennyami assertioni yaki nazivayetsya peredumovoyu metodu Dopustimi vidnosini mizh cimi stanami ta stanami yaki mozhut viniknuti v rezultati uspishnogo vikliku formalno opisuyutsya inshimi logichnimi tverdzhennyami pislyaumovi metodu Tak samo vidnosini mizh cimi poperednimi stanami i stanami yaki mozhut viniknuti v rezultati viniknennya viklyuchennya opisani vinyatkovim pislyaumovami exceptional postconditions metodu Stani dlya yakih metod ne povinen povertati znachennya opisuyutsya rozbizhnimi divergence umovami Odnak yavna zadannya takih umov vikoristovuyetsya v JML duzhe ridko Povedinka abstraktnogo tipu danih ATD yakij realizuyetsya za dopomogoyu klasiv Java viznachayetsya opisom naboru abstraktnih poliv dlya ob yektiv i opisom povedinki metodiv Abstraktni polya dlya ob yekta mozhut buti opisani abo za dopomogoyu modeli JML ta za dopomogoyu primarnih ghost poliv yaki vikoristovuyutsya tilki specifikaciyeyu abo vkazavshi dlya poliv realizaciyi anotaciyi spec public abo spec protected Taki anotaciyi dozvolyayut specifikatoru z dopomogoyu JML zmodelyuvati ob yekt u viglyadi kolekciyi abstraktnih poliv ob yektu podibno do takih mov yak Z 11 abo Fresco 12 Harakteristiki JML dodayutsya do Java kodu u viglyadi anotacij v komentaryah Java komentari interpretuyutsya yak Jml anotaciyi koli voni pochinayut zi znaka Tobto komentari viglyadu lt JML specification gt abo lt JML specification gt Osnovnij sintaksisOsnovnij sintaksis JML nadaye nastupni klyuchovi slova requires opisuye peredumovi ensures opisuye pislyaumovi signals opisuye pislyaumovu dlya vipadku koli viniklo zadane viklyuchennya u metodi signals only viznachaye yaki viklyuchennya mozhut buti kinuti koli vikonuyetsya zadana peredumova assignable viznachaye yakim polya mozhe buti prisvoyene znachennya v nastupnomu metodi pure ogoloshuye metod yakij ne produkuye pobichnih efektiv invariant viznachaye invariantnu neruhomist klasu loop invariant viznachaye invariant ciklu also poyednuye dekilka opisiv a takozh mozhe vkazuvati na te sho metod uspadkovuye opis vid svogo supertipu assert viznachaye vsyudi istinne tverdzhennya JML spec public robit zahishenu protected abo privatnu private zminnu dostupnoyu dlya potreb specifikaciyi result zadaye im ya dlya rezultatu old lt expression gt modifikator dlya zvernennya do znachennya lt expression gt na moment vhodu v metod forall lt decl gt lt range exp gt lt body exp gt kvantor dlya bud yakogo exists lt decl gt lt range exp gt lt body exp gt kvantor isnuvannya a gt b z a sliduye b a lt b a nasliduyetsya z b a lt gt b a todi i tilki todi koli b a takozh standartnij sintaksis Java dlya logichnogo I ABO i NI JML anotaciyi takozh mayut dostup do ob yektiv Java metodiv ob yektiv i operatoriv yaki v ramkah metodu anotuyutsya i mayut vidpovidnu vidimist Taka sukupnist dozvolyaye opisuvati formalni specifikaciyi vlastivostej klasiv poliv i metodiv Napriklad priklad prostogo bankivskogo klasu public class BankingExample public static final int MAX BALANCE 1000 private spec public int balance private spec public boolean isLocked false public invariant balance gt 0 amp amp balance lt MAX BALANCE assignable balance ensures balance 0 public BankingExample this balance 0 requires 0 lt amount amp amp amount balance lt MAX BALANCE assignable balance ensures balance old balance amount public void credit final int amount this balance amount requires 0 lt amount amp amp amount lt 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 Perevagi ta nedoliki JMLJML ce formalna mova specifikaciyi z priv yazkoyu do Java Takim chinom yiyi osnovne vikoristannya formalnij opis povedinki moduliv Java zastosunkiv Tak yak JML ce povedinkova mova specifikaciyi interfejsu yaka opisuye sposib vikoristannya okremih moduliv za mezhami Java zastosunkiv vona ne priznachenij dlya opisu povedinki vsiyeyi programi zagalom Tak pitannya Dlya chogo JML krashe pidhodit dijsno zvoditsya do nastupnogo pitannya sho horoshogo daye formalna specifikaciya programnih moduliv Java Dvi golovni perevagi vikoristanni JML tochnij odnoznachnij opis povedinki programnih moduliv na Java tobto klasiv i interfejsiv i dokumentuvannya kodu Java mozhlivist instrumentiv pidtrimki 13 Hocha mi hotili b instrumenti yaki dopomozhut z paralelnim programuvannyam program Java potochna versiya JML fokusuyetsya na poslidovnomu povedinci Java kodu U toj chas yak robota trivaye z rozshirennya JML dlya pidtrimki paralelizmu 14 potochna versiya JML ne maye funkciyi yaka dopomozhe viznachiti yak Java potoki vzayemodiyut odin z odnim Z tochki zoru detalnoyi proektnoyi dokumentaciyi specifikaciya JML mozhe nadati zovsim formalnij opis interfejsu i jogo poslidovnoyi povedinki Meta JML zrobiti zapis bajduzhim do tochnih metodiv programuvannya Mozhna vikoristovuvati JML abo dlya koduvannya abo dokumentaciyi gotovogo kodu Prichini dlya oficijnoyi dokumentaciyi interfejsiv i yih povedinki vikoristovuyuchi JML vklyuchayut v sebe nastupne Mozhna vidpraviti ob yektnij kod biblioteki klasiv kliyentu vidpravlyati specifikaciyi Jml ale ne vihidnij kod Kliyenti otrimayut dokumentaciyu yaka ye tochnoyu odnoznachnoyu ale ne nadmirno konkretnoyu Kliyenti ne matimut kod zahistu prav vlasnosti Krim togo kliyenti ne budut pokladatisya na detali realizaciyi biblioteki polegshuyuchi proces polipshennya kodu v majbutnih versiyah Mozhna vikoristovuvati specifikaciyu JML yak dopomogu dlya retelnogo obmirkuvannya pravilnosti kodu abo navit dlya formalnoyi verifikaciyi 15 Tehnichni harakteristiki JML mozhut vikoristovuvatis dekilkoma instrumentami yaki mozhut dopomogti nalagoditi i polipshiti kod 16 DzherelaJohn 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 LankiJava Modeling Language angl

Дата публікації:
Топ