Portal de Periódicos da CAPES

JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML

2008; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-540-87873-5_9

1611-3349

Patrice Chalin, Perry R. James, George Karabotsos,

Formal Methods in Verification

Tool support for the Java Modeling Language (JML) is a very pressing problem. A main issue with current tools is their architecture: the cost of keeping up with the evolution of Java is prohibitively high: e.g., Java 5 has yet to be fully supported. This paper presents JML4, our proposal for an Integrated Verification Environment (IVE) for JML that builds upon Eclipse's support for Java, enhancing it with Run time Assertion Checking (RAC), Extended Static Checking (ESC) and Full Static Program Verification (FSPV). Though it currently only supports a subset of JML, we believe that JML4 is the first IVE to support such a full range of verification techniques for a mainstream programming language.