Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
ESC/Java (және соңғы уақытта ESC/Java2), "Extended Static Checker for Java" – Java бағдарламаларында компиляция кезінде кездесетін жиі қателерді табуға бағытталған бағдарламалау құралы. ESC/Java-да қолданылатын негізгі тәсіл кеңейтілген статикалық тексеру деп аталады, ол әртүрлі бағдарламалық шектеулердің дұрыстығын статикалық түрде тексеруге арналған әдістердің жиынтығы. Мысалы, бүтін сан айнымалысы нөлден үлкен болуы немесе массив шегінде жатуы мүмкін. Бұл техника ESC/Java (және оның алдындағы ESC/Modula 3) құралында алғаш рет пайда болды және оны типтік тексерудің кеңейтілген түрі деп қарастыруға болады. Кеңейтілген статикалық тексеру әдетте автоматтандырылған теореманы дәлелдеушіні (theorem prover) пайдалануды қамтиды, ал ESC/Java құралында Simplify теореманы дәлелдеушісі қолданылды. ESC/Java толыққанды да, қатесіз де емес. Бұл қасақана жасалған, бағдарламашыға берілетін қателер мен ескертулер санын азайтуға және құралды практикалық тұрғыда тиімді етуге бағытталған. Дегенмен, бұл мынаны білдіреді: біріншіден, ESC/Java кейбір бағдарламаларды қате деп дұрыс емес тұжырымдайды (жалған оң нәтижелер); екіншіден, ол дұрыс емес бағдарламаларды дұрыс деп табады (жалған теріс нәтижелер). Соңғы санатқа модульдік арифметика және/немесе көп жіптілік (multithreading) қателері жатады. ESC/Java бастапқыда Compaq Systems Research Center (SRC) орталығында әзірленген. SRC жобаны 1997 жылы бастады, бұл олардың алғашқы кеңейтілген статикалық тексерушісі ESC/Modula 3 жұмысы 1996 жылы аяқталғаннан кейін болды. 2002 жылы SRC ESC/Java және оған байланысты құралдардың бастапқы кодын жариялады. ESC/Java құралының соңғы нұсқалары Java Модельдеу Тіліне (JML) негізделген. Пайдаланушылар бағдарламаларына арнайы форматталған түсініктемелер немесе прагмалар қосып, тексерудің көлемін және түрлерін басқара алады. Ниймеген университетінің Жүйелер қауіпсіздігі тобы 2004 жылға дейін JML спецификация тілін өңдейтін ESC/Java2 құралының кеңейтілген нұсқасының альфа нұсқасын шығарды. 2004 жылдан 2009 жылға дейін ESC/Java2 әзірлеуімен Дублин университетінің Университет колледжіндегі KindSoftware Research Group айналысты, ол 2009 жылы Копенгагеннің Ақпараттық технологиялар университетіне, ал 2012 жылы Дания Техникалық университетіне көшті. Ұзақ жылдар бойы ESC/Java2 көптеген жаңа мүмкіндіктерге ие болды, соның ішінде бірнеше теореманы дәлелдеушілермен жұмыс істеу және Eclipse ортасымен интеграциялау мүмкіндігі. OpenJML, ESC/Java2 құралының мұрагері, Java 1.8 нұсқасы үшін қолжетімді. Кодты мына мекенжайда табуға болады: https://github.com/OpenJML.
ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extended static checking, which is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater than zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java (and its predecessor, ESC/Modula 3) and can be thought of as an extended form of type checking. Extended static checking usually involves the use of an automated theorem prover and, in ESC/Java, the Simplify theorem prover was used. ESC/Java is neither sound nor complete. This was intentional and aims to reduce the number of errors and/or warnings reported to the programmer, in order to make the tool more useful in practice. However, it does mean that: firstly, there are programs that ESC/Java will erroneously consider to be incorrect (known as false positives); secondly, there are incorrect programs it will consider to be correct (known as false negatives). Examples in the latter category include errors arising from modular arithmetic and/or multithreading. ESC/Java was originally developed at the Compaq Systems Research Center (SRC). SRC launched the project in 1997, after work on their original extended static checker, ESC/Modula 3, ended in 1996. In 2002, SRC released the source code for ESC/Java and related tools. Recent versions of ESC/Java are based around the Java Modeling Language (JML). Users can control the amount and kinds of checking by annotating their programs with specially formatted comments or pragmas. The University of Nijmegen's Security of Systems group released alpha versions of ESC/Java2, an extended version of ESC/Java that processes the JML specification language through 2004. From 2004 to 2009, ESC/Java2 development was managed by the KindSoftware Research Group at University College Dublin, which in 2009 moved to the IT University of Copenhagen, and in 2012 to the Technical University of Denmark. Over the years, ESC/Java2 has gained many new features including the ability to reason with multiple theorem provers and integration with Eclipse. OpenJML, the successor of ESC/Java2, is available for Java 1.8. The source is available at https://github. com/OpenJML