ЭСК/Ява
 | Эта статья включает список общих ссылок , но в ней отсутствуют достаточные соответствующие встроенные цитаты . ( Март 2010 г. ) |
ESC/Java (а в последнее время ESC/Java2 ), «Расширенная программа статической проверки Java», представляет собой инструмент программирования , который пытается найти распространенные ошибки времени выполнения в Java программах во время компиляции . [1] Базовый подход, используемый в ESC/Java, называется расширенной статической проверкой . Это собирательное название, относящееся к ряду методов статической проверки правильности различных ограничений программы. Например, целочисленная переменная больше нуля или находится между границами массива . Этот метод был впервые использован в ESC/Java (и его предшественнике ESC/Modula-3) и может рассматриваться как расширенная форма проверки типов . Расширенная статическая проверка обычно включает использование автоматического средства доказательства теорем , а в ESC/Java использовалось средство доказательства теорем Simplify.
ESC/Java не является ни надежным , ни полным . Это было сделано намеренно и направлено на уменьшение количества ошибок и/или предупреждений, сообщаемых программисту, чтобы сделать инструмент более полезным на практике. Однако это означает, что: во-первых, существуют программы, которые ESC/Java ошибочно посчитает неправильными (известные как ложные срабатывания ); во-вторых, существуют неправильные программы, которые он считает правильными (так называемые ложноотрицательные ). Примеры последней категории включают ошибки, возникающие из-за модульной арифметики и/или многопоточности .
ESC/Java изначально был разработан в Исследовательском центре систем Compaq (SRC). SRC запустила проект в 1997 году, после того как работа над их оригинальной расширенной статической проверкой ESC/Modula-3 завершилась в 1996 году. В 2002 году SRC выпустила исходный код для ESC/Java и связанных с ним инструментов. Последние версии ESC/Java основаны на языке моделирования Java (JML). Пользователи могут контролировать объем и виды проверок, комментируя свои программы специально отформатированными комментариями или прагмами .
Университета Неймегена Группа безопасности систем выпустила альфа-версии ESC/Java2, расширенной версии ESC/Java, которая обрабатывает язык спецификации JML до 2004 года. С 2004 по 2009 год разработкой ESC/Java2 руководила исследовательская группа KindSoftware. в Университетском колледже Дублина , который в 2009 году перешёл в IT-университет Копенгагена , а в 2012 году — в Технический университет Дании . За прошедшие годы ESC/Java2 приобрел множество новых функций, включая возможность рассуждать с помощью нескольких средств доказательства теорем и интеграцию с Eclipse .
OpenJML , преемник ESC/Java2, доступен для Java 1.8. [2] Исходный код доступен по адресу https://github.com/OpenJML.
См. также
[ редактировать ]- Язык моделирования Java (JML)
Ссылки
[ редактировать ]- ^ Фланаган, К.; Лейно, КРМ; Лиллибридж, М.; Нельсон, Г .; Сакс, JB ; Стата, Р. (2002). Расширенная статическая проверка для Java . Материалы конференции по проектированию и реализации языков программирования . стр. 234–245. дои : 10.1145/512529.512558 . ISBN 1-58113-463-0 .
- ^ «Сайт загрузки OpenJML на sourceforge» .
- ^ «Язык моделирования Java (JML)/Код/[r9606]/OpenJML/Trunk/OpenJML» .
- Примечания
- Фланаган, К.; Кинири, КРМ (2001). Houdini, помощник по аннотациям для ESC/Java . FME 2001: Формальные методы повышения производительности программного обеспечения . стр. 500–517. дои : 10.1007/3-540-45251-6_29 . ISBN 3-540-41791-5 .
- Катаньо, Н.; Хейсман, М. (2002). Формальная спецификация и статическая проверка электронного кошелька Gemplus с использованием ESC/Java . FME 2002: Формальные методы – все правильно . стр. 272–289. дои : 10.1007/3-540-45614-7_16 . ISBN 3-540-43928-5 .
- Кок, ДР; Кинири, младший (2005). ESC/Java2: объединение ESC/Java и JML . Материалы международной конференции 2004 г. по созданию и анализу безопасных, защищенных и совместимых интеллектуальных устройств . стр. 108–128. дои : 10.1007/978-3-540-30569-9_6 . ISBN 3-540-24287-2 .
- Чалин, П.; Кинири, младший; Ливенс, GT; Полл, Э. (2006). За пределами утверждений: расширенная спецификация и проверка с помощью JML и ESC/Java2 . Формальные методы для компонентов и объектов . стр. 342–363 . дои : 10.1007/3-540-45614-7_16 . ISBN 3-540-36749-7 .
- Кок, ДР (2006). Указание итераторов Java с помощью JML и Esc/Java2 . Материалы конференции 2006 г. по спецификации и верификации компонентных систем . стр. 71–74. дои : 10.1145/1181195.1181210 . ISBN 1-59593-586-Х .
- Чалин, П. (2006). Раннее обнаружение ошибок спецификации JML с использованием ESC/Java2 . Материалы конференции 2006 г. по спецификации и верификации компонентных систем . стр. 25–32. дои : 10.1145/1181195.1181201 . ISBN 1-59593-586-Х .
- Исикава, Х. (2009). Подход к рефакторингу с использованием ESC/Java2: простой пример . Материалы конференции 2009 г. «Новые тенденции в методологиях, инструментах и методах программного обеспечения» . стр. 61–72. ISBN 978-1-60750-049-0 .
- Полл, Э. (2009). Спецификация и проверка программы обучения с использованием JML и ESC/Java2 (PDF) . Материалы 2-й Международной конференции по формальным методам обучения . стр. 92–104. дои : 10.1007/978-3-642-04912-5_7 . ISBN 978-3-642-04911-8 .
- Джеймс, PR; Чалин, П. (2009). ESC4: современный кеширующий ESC для Java . Материалы 8-го международного семинара «Спецификация и верификация компонентных систем» . стр. 19–26. дои : 10.1145/1596486.1596491 . ISBN 978-1-60558-680-9 .
Внешние ссылки
[ редактировать ]- Выпуск исходного кода набора инструментов для программирования Java
- Расширенная статическая проверка Java на Wayback Machine (архивировано 8 декабря 2005 г.)
- ESC/Java2 в KindSoftware
- SRC-RR-159 Расширенная статическая проверка. - Дэвид Л. Детлефс, К. Рустан М. Лейно, Грег Нельсон, Джеймс Б. Сакс
- Расширенная статическая проверка Модулы-3 на Wayback Machine (архив от 28 февраля 2001 г.)
- Коллоквиум по расширенной статической проверке в области компьютерных наук и инженерии. Университет Вашингтона. 1999.