JML and Aspects: The Benefits of Instrumenting JML Features with AspectJ Export

@inproceedings{citeulike:3717156, abstract = {The Java Modeling Language (JML) is used to specify designs of Java classes and interfaces. To this end, JML has a rich set of features for specifying methods, including specification inheritance. Thus, the most fundamental motivation for employing JML is to improve functional software correctness of Java applications, and helps to reduce corrective maintenance effort of those applications. Previously, we presented a new JML compiler (a jmlc) that generates aspects (AspectJ) for contract enforcement. This paper describes the main reasons to instrument JML features with AspectJ, with particular emphasis on issues related to instrumentation code size — we also defined guidelines to use a jmlc that always generate compact instrumented code than the classical JML compiler (jmlc). In addition, we discuss the analogy between JML and AspectJ, and how the a jmlc also deals with Java ME applications, which is not possible with jmlc. Moreover, we implemented other JML features such as the new the new assertion semantics based on "strong validity" presented elsewhere. The paper includes studies to compare the final code generated by a jmlc with the one produced by jmlc. Results indicate that the overhead in code size produced by our compiler is very small when using the proposed guidelines, which is essential for Java ME applications.}, author = {Reb\^{e}lo, Henrique and Soares, Sergio and Lima, Ricardo and Borba, Paulo and Corn\'{e}lio, M\'{a}rcio}, citeulike-article-id = {3717156}, citeulike-linkout-0 = {http://www.eecs.ucf.edu/~leavens/SAVCBS/2008/papers/Rebelo-Soares-Lima-Borba-Cornelio.pdf}, journal = {Specification and Verification of Component-Based Systems}, keywords = {jml, run, time, verification}, month = {November}, pages = {11--18}, posted-at = {2008-11-27 13:17:24}, priority = {3}, title = {JML and Aspects: The Benefits of Instrumenting JML Features with AspectJ}, url = {http://www.eecs.ucf.edu/~leavens/SAVCBS/2008/papers/Rebelo-Soares-Lima-Borba-Cornelio.pdf}, year = {2008} }

TY - CONF ID - citeulike:3717156 L3 - citeulike-article-id:3717156 N2 - The Java Modeling Language (JML) is used to specify designs of Java classes and interfaces. To this end, JML has a rich set of features for specifying methods, including specification inheritance. Thus, the most fundamental motivation for employing JML is to improve functional software correctness of Java applications, and helps to reduce corrective maintenance effort of those applications. Previously, we presented a new JML compiler (a jmlc) that generates aspects (AspectJ) for contract enforcement. This paper describes the main reasons to instrument JML features with AspectJ, with particular emphasis on issues related to instrumentation code size — we also defined guidelines to use a jmlc that always generate compact instrumented code than the classical JML compiler (jmlc). In addition, we discuss the analogy between JML and AspectJ, and how the a jmlc also deals with Java ME applications, which is not possible with jmlc. Moreover, we implemented other JML features such as the new the new assertion semantics based on "strong validity" presented elsewhere. The paper includes studies to compare the final code generated by a jmlc with the one produced by jmlc. Results indicate that the overhead in code size produced by our compiler is very small when using the proposed guidelines, which is essential for Java ME applications. JF - Specification and Verification of Component-Based Systems EP - 18 TI - JML and Aspects: The Benefits of Instrumenting JML Features with AspectJ SP - 11 KW - jml KW - run KW - time KW - verification AU - Rebêlo, Henrique AU - Soares, Sergio AU - Lima, Ricardo AU - Borba, Paulo AU - Cornélio, Márcio PY - 2008/11// UR - http://www.eecs.ucf.edu/~leavens/SAVCBS/2008/papers/Rebelo-Soares-Lima-Borba-Cornelio.pdf ER -