ESC/Java- ESC/Java
ESC/Java (en meer recentelijk ESC/Java2 ), de "Extended Static Checker for Java", is een programmeertool die tijdens het compileren veelvoorkomende runtime-fouten in Java- programma's probeert te vinden . De onderliggende benadering die in ESC/Java wordt gebruikt, wordt uitgebreide statische controle genoemd , wat een verzamelnaam is die verwijst naar een reeks technieken voor het statisch controleren van de juistheid van verschillende programmabeperkingen. Bijvoorbeeld dat een integer-variabele groter is dan nul, of tussen de grenzen van een array ligt . Deze techniek werd ontwikkeld in ESC/Java (en zijn voorganger, ESC/Modula-3) en kan worden gezien als een uitgebreide vorm van typecontrole . Uitgebreide statische controle omvat meestal het gebruik van een geautomatiseerde stellingbewijzer en in ESC/Java werd de Simplify stellingbewijzer gebruikt.
ESC/Java is niet correct en ook niet compleet . Dit was opzettelijk en heeft tot doel het aantal fouten en/of waarschuwingen dat aan de programmeur wordt gemeld te verminderen, om de tool in de praktijk bruikbaarder te maken. Het betekent echter wel dat: ten eerste zijn er programma's die ESC/Java ten onrechte als onjuist beschouwen (bekend als false-positives ); ten tweede zijn er onjuiste programma's die het als correct beschouwt (bekend als false-negatives ). Voorbeelden in de laatste categorie zijn fouten die voortkomen uit modulaire rekenkunde en/of multithreading .
ESC/Java is oorspronkelijk ontwikkeld in het Compaq Systems Research Center (SRC). SRC lanceerde het project in 1997, nadat het werk aan hun oorspronkelijke uitgebreide statische checker, ESC/Modula-3, eindigde in 1996. In 2002 gaf SRC de broncode voor ESC/Java en gerelateerde tools vrij. Recente versies van ESC/Java zijn gebaseerd op de Java Modeling Language (JML). Gebruikers kunnen de hoeveelheid en soorten controles controleren door hun programma's te annoteren met speciaal opgemaakte opmerkingen of pragma's .
De Security of Systems- groep van de Universiteit van Nijmegen heeft tot en met 2004 alfaversies van ESC/Java2 uitgebracht, een uitgebreide versie van ESC/Java die de JML- specificatietaal verwerkt . Van 2004 tot 2009 werd de ontwikkeling van ESC/Java2 beheerd door de KindSoftware Research Group aan University College Dublin , dat in 2009 verhuisde naar de IT-universiteit van Kopenhagen , en in 2012 naar de Technische Universiteit van Denemarken . In de loop der jaren heeft ESC/Java2 veel nieuwe functies gekregen, waaronder de mogelijkheid om te redeneren met meerdere stellingbewijzers en integratie met Eclipse .
OpenJML , de opvolger van ESC/Java2, is beschikbaar voor Java 1.8. De bron is beschikbaar op https://github.com/OpenJML
Zie ook
- Java-modelleringstaal (JML)
Referenties
- Opmerkingen:
- Flanagan, C.; Kiniry, KRM (2001). Houdini, een annotatie-assistent voor ESC/Java . FME 2001: Formele methoden voor het verhogen van de softwareproductiviteit . blz. 500-517. doi : 10.1007/3-540-45251-6_29 . ISBN 3-540-41791-5.
- Catano, N.; Huisman, M. (2002). Formele specificatie en statische controle van de elektronische portemonnee van Gemplus met behulp van ESC/Java . FME 2002: Formele methoden: het goed doen . blz. 272-289. doi : 10.1007/3-540-45614-7_16 . ISBN 3-540-43928-5.
- Cok, DR; Kiniry, JR (2005). ESC/Java2: ESC/Java en JML samenbrengen . Proceedings van de internationale conferentie van 2004 over constructie en analyse van veilige, beveiligde en interoperabele slimme apparaten . blz. 108–128. doi : 10.1007/978-3-540-30569-9_6 . ISBN 3-540-24287-2.
- Chalin, P.; Kiniry, JR; Zuurdesem, GT; Opiniepeiling, E. (2006). Beyond Assertions: geavanceerde specificatie en verificatie met JML en ESC/Java2 . Formele methoden voor componenten en objecten . blz. 342-363 . doi : 10.1007/3-540-45614-7_16 . ISBN 3-540-36749-7.
- Cok, DR (2006). Java-iterators specificeren met JML en Esc/Java2 . Proceedings van de conferentie van 2006 over specificatie en verificatie van op componenten gebaseerde systemen . blz. 71-74. doi : 10.1145/1181195.1181210 . ISBN 1-59593-586-X.
- Chalin, P. (2006). Vroegtijdige detectie van JML-specificatiefouten met behulp van ESC/Java2 . Proceedings van de conferentie van 2006 over specificatie en verificatie van op componenten gebaseerde systemen . blz. 25-32. doi : 10.1145/1181195.1181201 . ISBN 1-59593-586-X.
- Ishikawa, H. (2009). Een aanpak voor refactoring met behulp van ESC/Java2: een eenvoudige casestudy . Proceedings van de conferentie van 2009 over nieuwe trends in softwaremethodologieën, -hulpmiddelen en -technieken . blz. 61-72. ISBN 978-1-60750-049-0.
- Opiniepeiling, E. (2009). Specificatie en verificatie van lesprogramma's met behulp van JML en ESC/Java2 (PDF) . Proceedings van de 2e internationale conferentie over formele onderwijsmethoden . blz. 92-104. doi : 10.1007/978-3-642-04912-5_7 . ISBN 978-3-642-04911-8.
- James, PR; Chalin, P. (2009). ESC4: een moderne caching ESC voor Java . Proceedings van de 8e internationale workshop over specificatie en verificatie van op componenten gebaseerde systemen . blz. 19-26. doi : 10.1145/1596486.1596491 . ISBN 978-1-60558-680-9.
Externe links
- Bronversie van Java Programming Toolkit
- Uitgebreide statische controle voor Java op de Wayback Machine (gearchiveerd op 8 december 2005)
- ESC/Java2 bij KindSoftware
- SRC-RR-159 Uitgebreide statische controle. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe
- Uitgebreide statische controle Modula-3 bij de Wayback Machine (gearchiveerd 28 februari 2001)
- Uitgebreide statische controle Computer Science & Engineering Colloquia. Universiteit van Washington. 1999.
