ESC/Java - ESC/Java
ESC/Java (e più recentemente ESC/Java2 ), "Extended Static Checker for Java", è uno strumento di programmazione che tenta di trovare errori di runtime comuni nei programmi Java in fase di compilazione . L'approccio sottostante utilizzato in ESC/Java è indicato come controllo statico esteso , che è un nome collettivo che si riferisce a una serie di tecniche per il controllo statico della correttezza dei vari vincoli del programma. Ad esempio, una variabile intera è maggiore di zero o si trova tra i limiti di un array . Questa tecnica è stata introdotta in ESC/Java (e nel suo predecessore, ESC/Modula-3) e può essere pensata come una forma estesa di controllo del tipo . Il controllo statico esteso di solito comporta l'uso di un dimostratore di teoremi automatizzato e, in ESC/Java, è stato utilizzato il dimostratore di teoremi Simplify.
ESC/Java non è né sano né completo . Questo era intenzionale e mira a ridurre il numero di errori e/o avvisi segnalati al programmatore, al fine di rendere lo strumento più utile nella pratica. Tuttavia, significa che: in primo luogo, ci sono programmi che ESC/Java considereranno erroneamente non corretti (noti come falsi positivi ); in secondo luogo, ci sono programmi errati che considererà corretti (noti come falsi negativi ). Esempi in quest'ultima categoria includono errori derivanti dall'aritmetica modulare e/o dal multithreading .
ESC/Java è stato originariamente sviluppato presso il Compaq Systems Research Center (SRC). SRC ha lanciato il progetto nel 1997, dopo che il lavoro sul loro correttore statico esteso originale, ESC/Modula-3, è terminato nel 1996. Nel 2002, SRC ha rilasciato il codice sorgente per ESC/Java e strumenti correlati. Le versioni recenti di ESC/Java si basano sul Java Modeling Language (JML). Gli utenti possono controllare la quantità e il tipo di controllo annotando i loro programmi con commenti o pragma appositamente formattati .
L' Università di Nijmegen 's sicurezza dei sistemi gruppo ha pubblicato le versioni alpha di ESC / Java2, una versione estesa di ESC / Java che elabora il JML linguaggio di specifica attraverso 2004. Dal 2004 al 2009, lo sviluppo ESC / Java2 è stato gestito dal Gruppo di Ricerca KindSoftware allo University College Dublin , che nel 2009 si è trasferito all'Università IT di Copenhagen , e nel 2012 alla Technical University of Denmark . Nel corso degli anni, ESC/Java2 ha acquisito molte nuove funzionalità tra cui la capacità di ragionare con più dimostratori di teoremi e l'integrazione con Eclipse .
OpenJML , il successore di ESC/Java2, è disponibile per Java 1.8. La fonte è disponibile su https://github.com/OpenJML
Guarda anche
Riferimenti
- Appunti
- Flanagan, C.; Kiniry, KRM (2001). Houdini, un assistente per le annotazioni per ESC/Java . FME 2001: metodi formali per aumentare la produttività del software . pp. 500-517. doi : 10.1007/3-540-45251-6_29 . ISBN 3-540-41791-5.
- Catano, N.; Huisman, M. (2002). Specifiche formali e controllo statico della borsa elettronica di Gemplus mediante ESC/Java . FME 2002: Metodi formali: come farlo bene . pp. 272-289. doi : 10.1007/3-540-45614-7_16 . ISBN 3-540-43928-5.
- Cok, DR; Kiniry, JR (2005). ESC/Java2: unire ESC/Java e JML . Atti della conferenza internazionale 2004 sulla costruzione e l'analisi di dispositivi intelligenti sicuri, protetti e interoperabili . pp. 108-128. doi : 10.1007/978-3-540-30569-9_6 . ISBN 3-540-24287-2.
- Chalin, P.; Kiniry, JR; lieviti, GT; Sondaggio, E. (2006). Oltre le asserzioni: specifica avanzata e verifica con JML e ESC/Java2 . Metodi formali per componenti e oggetti . pp. 342-363 . doi : 10.1007/3-540-45614-7_16 . ISBN 3-540-36749-7.
- Cok, DR (2006). Specifica di iteratori java con JML e Esc/Java2 . Atti del convegno 2006 su Specificazione e verifica dei sistemi basati su componenti . pp. 71-74. doi : 10.1145/1181195.1181210 . ISBN 1-59593-586-X.
- Chalin, P. (2006). Rilevamento precoce degli errori di specifica JML utilizzando ESC/Java2 . Atti del convegno 2006 su Specificazione e verifica dei sistemi basati su componenti . pp. 25-32. doi : 10.1145/1181195.1181201 . ISBN 1-59593-586-X.
- Ishikawa, H. (2009). Un approccio per il refactoring utilizzando ESC/Java2: un semplice caso di studio . Atti del convegno 2009 sulle nuove tendenze nelle metodologie, strumenti e tecniche del software . pp. 61-72. ISBN 978-1-60750-049-0.
- Sondaggio, E. (2009). Specificazione e verifica del programma di insegnamento mediante JML e ESC/Java2 (PDF) . Atti del 2° Convegno Internazionale sui metodi formali di insegnamento . pp. 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 di memorizzazione nella cache per Java . Atti dell'8° workshop internazionale su Specificazione e verifica dei sistemi basati su componenti . pp. 19-26. doi : 10.1145/1596486.1596491 . ISBN 978-1-60558-680-9.
link esterno
- Rilascio del codice sorgente del toolkit di programmazione Java
- Controllo statico esteso per Java presso la Wayback Machine (archiviato l'8 dicembre 2005)
- ESC/Java2 su KindSoftware
- SRC-RR-159 Controllo statico esteso. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe
- Controllo statico esteso Modula-3 alla Wayback Machine (archiviato il 28 febbraio 2001)
- Colloqui di informatica e ingegneria sul controllo statico esteso . Università di Washington. 1999.
