OpenJML: JML for Java']Java 7 by Extending OpenJDK

被引：0
|
作者：
Cok, David R. [1 ]
机构：
[1] GrammaTech Inc, Ithaca, NY 14850 USA
来源：
NASA FORMAL METHODS | 2011年 / 6617卷
关键词：
OpenJML; JML; specification; verification; OpenJDK; ESC/[!text type='Java']Java[!/text]2; SYSTEM;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The Java Modeling Language is a widely used specification language for Java. However, the tool support has not kept pace with advances in the Java language. This paper describes OpenJML, an implementation of JML tools built by extending the OpenJDK Java tool set. OpenJDK has a readily extendible architecture, though its details could be revised to further facilitate extension. The result is a suite of JML tools for Java 7 that provides static analysis, specification documentation, and runtime checking, an API that is used for other tools, uses Eclipse as an IDE, and can be extended for further research. In addition, OpenJML can leverage the community effort devoted to OpenJDK.
引用
收藏
页码：472 / 479
页数：8
相关论文
共 50 条
  • [1] OpenJML: JML for Java 7 by extending OpenJDK
    Cok, David R.
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2011, 6617 LNCS : 472 - 479
  • [2] OpenJML: Software verification for Java']Java 7 using JML, OpenJDK, and Eclipse
    Cok, David R.
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (149): : 79 - 92
  • [3] JML and OpenJML for Java']Java 16
    Cok, David R.
    [J]. PROCEEDINGS OF THE 23RD ACM INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP '21), 2021, : 65 - 67
  • [4] A formal specification in JML of Java']Java security package
    Agarwal, Poonam
    Rubio-Medrano, Carlos E.
    Cheon, Yoonsik
    Teller, Patricia. J.
    [J]. ADVANCES AND INNOVATIONS IN SYSTEMS, COMPUTING SCIENCES AND SOFTWARE ENGINEERING, 2007, : 363 - 368
  • [5] On extending Java']Java
    Krall, A
    Vitek, J
    [J]. MODULAR PROGRAMMING LANGUAGES, 1997, 1204 : 321 - 335
  • [6] The KRAKATOA tool for certification of JAVA']JAVA/JAVA']JAVACARD programs annotated in JML
    Marché, C
    Paulin-Mohring, C
    Urbain, X
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2004, 58 (1-2): : 89 - 106
  • [7] The LOOP compiler for java and JML
    Computing Science Institute, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, Netherlands
    [J]. Lect. Notes Comput. Sci., 1600, (299-312):
  • [8] Automated translation of VDM to JML-annotated Java']Java
    Tran-Jorgensen, Peter W. V.
    Larsen, Peter Gorm
    Leavens, Gary T.
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2018, 20 (02) : 211 - 235
  • [9] Measuring a Java']Java Test Suite Coverage Using JML Specifications
    Dadeau, F.
    Ledru, Y.
    du Bousqueta, L.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 190 (02) : 21 - 32
  • [10] JML4: Towards an Industrial Grade IVE for Java']Java and Next Generation Research Platform for JML
    Chalin, Patrice
    James, Perry R.
    Karabotsos, George
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 5295 : 70 - 83
12345