ESC / Java (y más recientemente ESC / Java2 ), el "Comprobador estático extendido para Java", es una herramienta de programación que intenta encontrar errores comunes en tiempo de ejecución en programas Java en tiempo de compilación . [1] El enfoque subyacente utilizado en ESC / Java se conoce como verificación estática extendida , que es un nombre colectivo que se refiere a una gama de técnicas para verificar estáticamente la corrección de varias restricciones del programa. Por ejemplo, que una variable entera es mayor que cero o se encuentra entre los límites de una matriz. Esta técnica fue pionera en ESC / Java (y su predecesor, ESC / Modula-3) y se puede considerar como una forma extendida de verificación de tipos . La verificación estática extendida generalmente implica el uso de un probador de teoremas automatizado y, en ESC / Java, se utilizó el probador de teoremas Simplify.
ESC / Java no es sólido ni completo . Esto fue intencional y tiene como objetivo reducir la cantidad de errores y / o advertencias informadas al programador, para que la herramienta sea más útil en la práctica. Sin embargo, sí significa que: en primer lugar, hay programas que ESC / Java considerará erróneamente como incorrectos (conocidos como falsos positivos ); en segundo lugar, hay programas incorrectos que considerará correctos (conocidos como falsos negativos ). Los ejemplos en la última categoría incluyen errores que surgen de aritmética modular y / o subprocesos múltiples .
ESC / Java se desarrolló originalmente en el Centro de Investigación de Sistemas de Compaq (SRC). SRC lanzó el proyecto en 1997, después de que el trabajo en su verificador estático extendido original, ESC / Modula-3, terminara en 1996. En 2002, SRC lanzó el código fuente para ESC / Java y herramientas relacionadas. Las versiones recientes de ESC / Java se basan en Java Modeling Language (JML). Los usuarios pueden controlar la cantidad y los tipos de comprobación anotando sus programas con comentarios o pragmas formateados especialmente .
La Universidad de Nijmegen 's seguridad de los sistemas lanzado versiones alfa del grupo de ESC / Java2, una versión extendida de ESC / Java que procesa la JML lenguaje de especificación hasta 2004. De 2004 a 2009, el desarrollo ESC / Java2 fue gestionado por el Grupo de Investigación KindSoftware en University College Dublin , que en 2009 se trasladó a la IT University of Copenhagen , y en 2012 a la Technical University of Denmark . A lo largo de los años, ESC / Java2 ha ganado muchas características nuevas, incluida la capacidad de razonar con múltiples probadores de teoremas y la integración con Eclipse .
OpenJML , el sucesor de ESC / Java2, está disponible para Java 1.8. [2] La fuente está disponible en https://github.com/OpenJML.
Ver también
Referencias
- ↑ Flanagan, C .; Leino, KRM; Lillibridge, M .; Nelson, G .; Saxe, JB ; Stata, R. (2002). Comprobación estática ampliada para Java . Actas de la conferencia sobre diseño e implementación de lenguajes de programación . págs. 234–245. doi : 10.1145 / 512529.512558 . ISBN 1-58113-463-0.
- ^ http://jmlspecs.sourceforge.net/
- ^ https://sourceforge.net/p/jmlspecs/code/HEAD/tree/OpenJML/trunk/OpenJML/
- Notas
- Flanagan, C .; Kiniry, KRM (2001). Houdini, asistente de anotaciones para ESC / Java . FME 2001: Métodos formales para aumentar la productividad del software . págs. 500–517. doi : 10.1007 / 3-540-45251-6_29 . ISBN 3-540-41791-5.
- Cataño, N .; Huisman, M. (2002). Especificación formal y verificación estática del monedero electrónico de Gemplus mediante ESC / Java . FME 2002: Métodos formales: hacerlo bien . págs. 272-289. doi : 10.1007 / 3-540-45614-7_16 . ISBN 3-540-43928-5.
- Cok, DR; Kiniry, JR (2005). ESC / Java2: uniendo ESC / Java y JML . Actas de la conferencia internacional de 2004 sobre construcción y análisis de dispositivos inteligentes seguros, protegidos e interoperables . págs. 108-128. doi : 10.1007 / 978-3-540-30569-9_6 . ISBN 3-540-24287-2.
- Chalin, P .; Kiniry, JR; Levaduras, GT; Encuesta, E. (2006). Más allá de las afirmaciones: Especificación y verificación avanzadas con JML y ESC / Java2 . Métodos formales para componentes y objetos . págs. 342–363 . doi : 10.1007 / 3-540-45614-7_16 . ISBN 3-540-36749-7.
- Cok, DR (2006). Especificación de iteradores de Java con JML y Esc / Java2 . Actas de la conferencia de 2006 sobre especificación y verificación de sistemas basados en componentes . págs. 71–74. doi : 10.1145 / 1181195.1181210 . ISBN 1-59593-586-X.
- Chalin, P. (2006). Detección temprana de errores de especificación JML usando ESC / Java2 . Actas de la conferencia de 2006 sobre especificación y verificación de sistemas basados en componentes . págs. 25–32. doi : 10.1145 / 1181195.1181201 . ISBN 1-59593-586-X.
- Ishikawa, H. (2009). Un enfoque para la refactorización utilizando ESC / Java2: un estudio de caso simple . Actas de la conferencia de 2009 sobre nuevas tendencias en metodologías, herramientas y técnicas de software . págs. 61–72. ISBN 978-1-60750-049-0.
- Encuesta, E. (2009). Especificación y verificación de programas de enseñanza mediante JML y ESC / Java2 (PDF) . Actas del II Congreso Internacional de Enseñanza de Métodos Formales . págs. 92-104. doi : 10.1007 / 978-3-642-04912-5_7 . ISBN 978-3-642-04911-8.
- James, PR; Chalin, P. (2009). ESC4: un moderno ESC de almacenamiento en caché para Java . Actas del 8º taller internacional sobre especificación y verificación de sistemas basados en componentes . págs. 19-26. doi : 10.1145 / 1596486.1596491 . ISBN 978-1-60558-680-9.
enlaces externos
- Versión de origen del kit de herramientas de programación Java
- Comprobación estática ampliada para Java en Wayback Machine (archivado el 8 de diciembre de 2005)
- ESC / Java2 en KindSoftware
- SRC-RR-159 Verificación estática extendida. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe
- Extended Static Checking Modula-3 en Wayback Machine (archivado el 28 de febrero de 2001)
- Coloquios extendidos de ingeniería y ciencias de la computación de verificación estática . Universidad de Washington. 1999.