Кіріспе

Java бағдарламалары үшін спецификация тілі

Java Modeling Language (JML) – Java бағдарламалары үшін спецификация тілі болып табылады, ол Hoare стиліндегі алғы және кейінгі шарттарды, инварианттарды қолданады және келісім-шарт бойынша жобалау парадигмасын ұстанады. Спецификациялар бастапқы файлдарға Java түсініктемелері түрінде жазылады, осылайша оларды кез келген Java компиляторымен жинастыруға болады. Дамуға түрлі тексеру құралдары көмектеседі, мысалы, орындалу кезіндегі нақтылықты тексеруші және кеңейтілген статикалық тексеруші (ESC/Java).

Шолу

JML – Java модульдері үшін мінез-құлық интерфейсін сипаттау тілі. JML Java модулінің қызметін формалды түрде сипаттауға арналған семантиканы ұсынады, модульді жасаушылардың мақсаттарына қатысты екіұштылықтарды болдырмайды. JML идеяларын Эйфель, Ларх және Нақтылау есептеуінен сіңіреді, мақсаты – кез келген Java бағдарламашысына қолжетімді болып, қатаң формалды семантиканы қамтамасыз ету. JML-дің мінез-құлық сипаттамаларын пайдаланатын түрлі құралдар бар. Сипаттамалар Java бағдарлама файлдарында түсініктемелер түрінде немесе жеке сипаттама файлдарында сақталуы мүмкін болғандықтан, JML сипаттамалары бар Java модульдерін кез келген Java компиляторымен өзгеріссіз жинастыруға болады.

Құралдарды қолдау

Әртүрлі құралдар JML аннотацияларына негізделген функционалдылықты қамтамасыз етеді. Айова штатының JML құралдары JML түсіндірмелерін орындалу кезіндегі тексерулерге айналдыратын jmlc мәлімдемелерді тексеру компиляторын, JML түсіндірмелерінен қосымша ақпарат алатын Javadoc құжаттамасын жасайтын jmldoc құжаттама генераторын және JML түсіндірмелерінен JUnit сынақ кодын жасайтын jmlunit бірлік сынақ генераторын ұсынады. Тәуелсіз топтар JML аннотацияларын пайдаланатын құралдарды жасауда. Оларға: ESC/Java2, JML аннотацияларын пайдаланып, басқа жағдайда мүмкін емес қатаң статикалық тексеруді жүзеге асыратын кеңейтілген статикалық тексеруші. OpenJML өзін ESC/Java2-нің жалғасы деп жариялайды. Daikon – динамикалық инварианттар генераторы. KeY, ол JML алдыңғы интерфейсімен және JML синтаксисін ерекшелендіретін Eclipse плагинімен (JML редакциялау) ашық кодты теореманы дәлелдейтін құралды ұсынады. Krakatoa, Why тексеру платформасына негізделген және Coq дәлелдеу көмекшісін пайдаланатын статикалық тексеру құралы. JMLEclipse, JML синтаксисін қолдайтын және JML аннотацияларын пайдаланатын әртүрлі құралдарға интерфейстері бар Eclipse интеграцияланған даму ортасы үшін плагин. Sireum/Kiasan, JML-ді келісім-шарт тілі ретінде қолдайтын, символды орындауға негізделген статикалық талдаушы. JMLUnit, JML түсіндірмелері бар Java файлдарында JUnit сынақтарын іске қосу үшін файлдарды жасайтын құрал. TACO, Java бағдарламасының Java Modeling Language спецификациясына сәйкестігін статикалық түрде тексеретін ашық кодты бағдарлама талдау құралы.