ESC/Java - ESC/Java
ESC/Java (og mer nylig ESC/Java2 ), "Extended Static Checker for Java", er et programmeringsverktøy som prøver å finne vanlige kjøretidsfeil i Java- programmer ved kompileringstidspunktet . Den underliggende tilnærmingen som brukes i ESC/Java omtales som utvidet statisk kontroll , som er et samlingsnavn som refererer til en rekke teknikker for statisk kontroll av riktigheten av ulike programbegrensninger. For eksempel at en heltallsvariabel er større enn null, eller ligger mellom grensene til en matrise . Denne teknikken var banebrytende innen ESC/Java (og forgjengeren, ESC/Modula-3) og kan betraktes som en utvidet form for typekontroll . Utvidet statisk kontroll innebærer vanligvis bruk av en automatisert setningsprover, og i ESC/Java ble Simplify theorem prover brukt.
ESC/Java er verken lyd eller komplett . Dette var tilsiktet og har som mål å redusere antall feil og/eller advarsler som er rapportert til programmereren, for å gjøre verktøyet mer nyttig i praksis. Imidlertid betyr det at: for det første er det programmer som ESC/Java feilaktig vil regne som feil (kjent som falsk-positive ); for det andre er det feil programmer det vil anse som riktige (kjent som falske-negative ). Eksempler i sistnevnte kategori inkluderer feil som oppstår fra modulær aritmetikk og/eller multitråding .
ESC/Java ble opprinnelig utviklet ved Compaq Systems Research Center (SRC). SRC startet prosjektet i 1997, etter at arbeidet med den opprinnelige utvidede statiske kontrolleren, ESC/Modula-3, ble avsluttet i 1996. I 2002 ga SRC ut kildekoden for ESC/Java og relaterte verktøy. Nylige versjoner av ESC/Java er basert på Java Modeling Language (JML). Brukere kan kontrollere mengden og typen kontroll ved å kommentere programmene sine med spesialformaterte kommentarer eller pragmer .
Den University of Nijmegen 's Security of Systems Group utgitt alfaversjoner av ESC / JAVA2, en utvidet versjon av ESC / Java som behandler JML spesifikasjon språk gjennom 2004. Fra 2004 til 2009, ESC / JAVA2 utvikling ble styrt av KindSoftware Research Group ved University College Dublin , som i 2009 flyttet til IT University of Copenhagen , og i 2012 til Danmarks tekniske universitet . Gjennom årene har ESC/Java2 fått mange nye funksjoner, inkludert evnen til å resonnere med flere teorem -bevisere og integrasjon med Eclipse .
OpenJML , etterfølgeren til ESC/Java2, er tilgjengelig for Java 1.8. Kilden er tilgjengelig på https://github.com/OpenJML
Se også
- Java -modelleringsspråk (JML)
Referanser
- Merknader
- Flanagan, C .; Kiniry, KRM (2001). Houdini, en annotasjonsassistent for ESC/Java . FME 2001: Formelle metoder for å øke programvareproduktiviteten . s. 500–517. doi : 10.1007/3-540-45251-6_29 . ISBN 3-540-41791-5.
- Cataño, N .; Huisman, M. (2002). Formell spesifikasjon og statisk kontroll av Gemplus 'elektroniske veske ved hjelp av ESC/Java . FME 2002: Formelle metoder - Få det riktig . s. 272–289. doi : 10.1007/3-540-45614-7_16 . ISBN 3-540-43928-5.
- Cok, DR; Kiniry, JR (2005). ESC/Java2: forener ESC/Java og JML . Prosedyrer fra den internasjonale konferansen i 2004 om konstruksjon og analyse av sikre, sikre og interoperable smarte enheter . s. 108–128. doi : 10.1007/978-3-540-30569-9_6 . ISBN 3-540-24287-2.
- Chalin, P .; Kiniry, JR; Leavens, GT; Poll, E. (2006). Utover påstander: Avansert spesifikasjon og verifikasjon med JML og ESC/Java2 . Formelle metoder for komponenter og objekter . s. 342–363 . doi : 10.1007/3-540-45614-7_16 . ISBN 3-540-36749-7.
- Cok, DR (2006). Spesifisere java iteratorer med JML og Esc/Java2 . Prosedyrer fra konferansen 2006 om spesifikasjon og verifikasjon av komponentbaserte systemer . s. 71–74. doi : 10.1145/1181195.1181210 . ISBN 1-59593-586-X.
- Chalin, P. (2006). Tidlig påvisning av JML -spesifikasjonsfeil ved bruk av ESC/Java2 . Prosedyrer fra konferansen 2006 om spesifikasjon og verifikasjon av komponentbaserte systemer . s. 25–32. doi : 10.1145/1181195.1181201 . ISBN 1-59593-586-X.
- Ishikawa, H. (2009). En tilnærming for refactoring ved bruk av ESC/Java2: En enkel casestudie . Fortsettelse av konferansen i 2009 om nye trender innen programvaremetoder, verktøy og teknikker . s. 61–72. ISBN 978-1-60750-049-0.
- Poll, E. (2009). Læringsprogramspesifikasjon og verifisering ved hjelp av JML og ESC/Java2 (PDF) . Prosedyrer fra den andre internasjonale konferansen om undervisning i formelle metoder . s. 92–104. doi : 10.1007/978-3-642-04912-5_7 . ISBN 978-3-642-04911-8.
- James, PR; Chalin, P. (2009). ESC4: en moderne hurtigbufring ESC for Java . Fortsettelse av den 8. internasjonale workshopen om spesifikasjon og verifikasjon av komponentbaserte systemer . s. 19–26. doi : 10.1145/1596486.1596491 . ISBN 978-1-60558-680-9.
Eksterne linker
- Java Programming Toolkit Source Release
- Utvidet statisk kontroll for Java på Wayback -maskinen (arkivert 8. desember 2005)
- ESC/Java2 på KindSoftware
- SRC-RR-159 Utvidet statisk kontroll. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe
- Utvidet statisk kontrollmodul-3 på Wayback-maskinen (arkivert 28. februar 2001)
- Utvidet statisk kontroll av datavitenskap og ingeniørvitenskap Colloquia. University of Washington. 1999.
