The Architecture of JML4, a Proposed Integrated Verification Environment for JML Export

@techreport{chalin07architecture, abstract = {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., almost three years following its release, Java 5 has yet to be fully supported. This paper presents the architecture of JML4, an Integrated Verification Environment (IVE) for JML that builds upon Eclipse's support for Java, enhancing it with Extended Static Checking (ESC), an early form of Runtime Assertion Checking (RAC) and JML's non-null type system. Early results indicate that the synergy of complementary verification techniques (being made available within a single tool) can help developers be more effective; we demonstrate new bugs uncovered in JML annotated Java source—like ESC/Java2— which is routinely verified using first generation JML tools.}, author = {Chalin, Patrice and James, Perry and Karabotsos, George}, citeulike-article-id = {1676032}, institution = {Department of Computer Science and Software Engineering, Concordia University}, keywords = {java, jml, jml4, softnet, specification, verification}, posted-at = {2007-09-19 14:39:06}, priority = {0}, title = {The Architecture of JML4, a Proposed Integrated Verification Environment for JML}, year = {2007} }

TY - RPRT ID - chalin07architecture L3 - citeulike-article-id:1676032 N2 - 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., almost three years following its release, Java 5 has yet to be fully supported. This paper presents the architecture of JML4, an Integrated Verification Environment (IVE) for JML that builds upon Eclipse’s support for Java, enhancing it with Extended Static Checking (ESC), an early form of Runtime Assertion Checking (RAC) and JML’s non-null type system. Early results indicate that the synergy of complementary verification techniques (being made available within a single tool) can help developers be more effective; we demonstrate new bugs uncovered in JML annotated Java source—like ESC/Java2— which is routinely verified using first generation JML tools. TI - The Architecture of JML4, a Proposed Integrated Verification Environment for JML KW - java KW - jml KW - jml4 KW - softnet KW - specification KW - verification AU - Chalin, Patrice AU - James, Perry AU - Karabotsos, George PY - 2007/// ER -