ESC / Java - ESC/Java
ESC / Java (e mais recentemente ESC / Java2 ), o "Extended Static Checker for Java", é uma ferramenta de programação que tenta encontrar erros comuns de tempo de execução em programas Java em tempo de compilação . A abordagem subjacente usada em ESC / Java é conhecida como verificação estática estendida , que é um nome coletivo que se refere a uma variedade de técnicas para verificar estaticamente a exatidão de várias restrições de programa. Por exemplo, que uma variável inteira é maior que zero ou está entre os limites de uma matriz . Essa técnica foi pioneira em ESC / Java (e seu predecessor, ESC / Modula-3) e pode ser considerada uma forma estendida de verificação de tipo . A verificação estática estendida geralmente envolve o uso de um provador de teoremas automatizado e, em ESC / Java, o provador de teoremas Simplify foi usado.
ESC / Java não é bom nem completo . Isso foi intencional e visa reduzir o número de erros e / ou avisos reportados ao programador, a fim de tornar a ferramenta mais útil na prática. No entanto, isso significa que: em primeiro lugar, existem programas que ESC / Java irá erroneamente considerar como incorretos (conhecidos como falsos positivos ); em segundo lugar, existem programas incorretos que serão considerados corretos (conhecidos como falsos negativos ). Os exemplos na última categoria incluem erros decorrentes da aritmética modular e / ou multithreading .
ESC / Java foi originalmente desenvolvido no Compaq Systems Research Center (SRC). A SRC lançou o projeto em 1997, após trabalhar em seu verificador estático estendido original, ESC / Modula-3, encerrado em 1996. Em 2002, a SRC lançou o código-fonte para ESC / Java e ferramentas relacionadas. Versões recentes de ESC / Java são baseadas em Java Modeling Language (JML). Os usuários podem controlar a quantidade e os tipos de verificação anotando seus programas com comentários ou pragmas especialmente formatados .
A Universidade de Nijmegen de segurança dos sistemas de grupo lançou versões alfa do ESC / Java2, uma versão estendida do ESC / Java que processa a JML linguagem de especificação até 2004. De 2004 a 2009, o desenvolvimento ESC / Java2 foi gerido pelo Grupo de Pesquisa KindSoftware na University College Dublin , que em 2009 se mudou para a IT University of Copenhagen , e em 2012 para a Technical University of Denmark . Ao longo dos anos, ESC / Java2 ganhou muitos novos recursos, incluindo a capacidade de raciocinar com vários provadores de teoremas e integração com o Eclipse .
OpenJML , o sucessor de ESC / Java2, está disponível para Java 1.8. A fonte está disponível em https://github.com/OpenJML
Veja também
- Java Modeling Language (JML)
Referências
- Notas
- Flanagan, C .; Kiniry, KRM (2001). Houdini, um assistente de anotação para ESC / Java . FME 2001: Métodos formais para aumentar a produtividade do software . pp. 500–517. doi : 10.1007 / 3-540-45251-6_29 . ISBN 3-540-41791-5.
- Cataño, N .; Huisman, M. (2002). Especificação formal e verificação estática do porta-moedas eletrônico da Gemplus usando ESC / Java . FME 2002: Métodos formais - Fazendo a TI da maneira certa . pp. 272–289. doi : 10.1007 / 3-540-45614-7_16 . ISBN 3-540-43928-5.
- Cok, DR; Kiniry, JR (2005). ESC / Java2: unindo ESC / Java e JML . Procedimentos da conferência internacional de 2004 sobre construção e análise de dispositivos inteligentes seguros, protegidos e interoperáveis . pp. 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). Além das afirmações: Especificação e verificação avançadas com JML e ESC / Java2 . Métodos formais para componentes e objetos . pp. 342–363 . doi : 10.1007 / 3-540-45614-7_16 . ISBN 3-540-36749-7.
- Cok, DR (2006). Especificando iteradores Java com JML e Esc / Java2 . Anais da conferência de 2006 sobre especificação e verificação de sistemas baseados em componentes . pp. 71–74. doi : 10.1145 / 1181195.1181210 . ISBN 1-59593-586-X.
- Chalin, P. (2006). Detecção precoce de erros de especificação JML usando ESC / Java2 . Anais da conferência de 2006 sobre especificação e verificação de sistemas baseados em componentes . pp. 25–32. doi : 10.1145 / 1181195.1181201 . ISBN 1-59593-586-X.
- Ishikawa, H. (2009). Uma abordagem para refatoração usando ESC / Java2: um estudo de caso simples . Anais da conferência de 2009 sobre Novas Tendências em Metodologias, Ferramentas e Técnicas de Software . pp. 61–72. ISBN 978-1-60750-049-0.
- Poll, E. (2009). Ensino de Especificação e Verificação de Programas em JML e ESC / Java2 (PDF) . Anais da 2ª Conferência Internacional sobre Métodos Formais de Ensino . pp. 92–104. doi : 10.1007 / 978-3-642-04912-5_7 . ISBN 978-3-642-04911-8.
- James, PR; Chalin, P. (2009). ESC4: um ESC de cache moderno para Java . Anais do 8º workshop internacional sobre Especificação e verificação de sistemas baseados em componentes . pp. 19–26. doi : 10.1145 / 1596486.1596491 . ISBN 978-1-60558-680-9.
links externos
- Versão fonte do kit de ferramentas de programação Java
- Verificação estática estendida para Java na máquina Wayback (arquivado em 8 de dezembro de 2005)
- ESC / Java2 em KindSoftware
- SRC-RR-159 Verificação estática estendida. - David L. Detlefs, K. Rustan M. Leino, Greg Nelson, James B. Saxe
- Extended Static Checking Modula-3 na Wayback Machine (arquivado em 28 de fevereiro de 2001)
- Verificação Estática Estendida de Ciência da Computação e Colóquios de Engenharia. Universidade de Washington. 1999.
