K-Java']Java: A Complete Semantics of Java']Java

被引：0
|
作者：
Bogdanas, Denis [1 ]
Rosu, Grigore [2 ]
机构：
[1] Alexandru Ioan Cuza Univ, Iasi, Romania
[2] Univ Illinois, Champaign, IL USA
来源：
ACM SIGPLAN NOTICES | 2015年 / 50卷 / 01期
关键词：
!text type='Java']Java[!/text; mechanized semantics; K framework; EXECUTABLE FORMAL SEMANTICS; DEFINITION;
D O I：
10.1145/2775051.2676982
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper presents K-Java, a complete executable formal semantics of Java 1.4. K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology. In order to maintain clarity while handling the great size of Java, the semantics was split into two separate definitions - a static semantics and a dynamic semantics. The output of the static semantics is a preprocessed Java program, which is passed as input to the dynamic semantics for execution. The preprocessed program is a valid Java program, which uses a subset of the features of Java. The semantics is applied to model-check multi-threaded programs. Both the test suite and the static semantics are generic and ready to be used in other Java-related projects.
引用
收藏
页码：445 / 456
页数：12
相关论文
共 50 条
  • [21] An operational semantics of Java']Java 2 access control
    Karjoth, G
    [J]. 13TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2000, : 224 - 232
  • [22] Java']Java/A - Taking components into Java']Java
    Hacklinger, F
    [J]. INTELLIGENT AND ADAPTIVE SYSTEMS AND SOFTWARE ENGINEERING, 2004, : 163 - 168
  • [23] Java']Java 2: The complete reference.
    Ziener, C
    [J]. LIBRARY JOURNAL, 2001, 126 (06) : 124 - 124
  • [24] Formalizing the safety of Java']Java, the Java']Java virtual machine, and Java']Java card
    Hartel, PH
    Moreau, L
    [J]. ACM COMPUTING SURVEYS, 2001, 33 (04) : 517 - 558
  • [25] Flow Java']Java: Declarative concurrency for Java']Java
    Drejhammar, F
    Schulte, C
    Brand, P
    Haridi, S
    [J]. LOGIC PROGRAMMING, PROCEEDINGS, 2003, 2916 : 346 - 360
  • [26] Java']Java: Coordination and communication for Java']Java agents
    Ciancarini, P
    Rossi, D
    [J]. MOBILE OBJECT SYSTEMS: TOWARDS THE PROGRAMMABLE INTERNET, 1997, 1222 : 213 - 226
  • [27] A dualthreaded Java']Java processor for Java']Java multithreading
    Chung, CM
    Kim, SD
    [J]. 1998 INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED SYSTEMS, PROCEEDINGS, 1998, : 693 - 700
  • [28] On the semantics of java']javaspaces
    Busi, N
    Gorrieri, R
    Zavattaro, G
    [J]. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV, 2000, 49 : 3 - 19
  • [29] Java']Java
    不详
    [J]. IEEE INTERNET COMPUTING, 1999, 3 (02) : 13 - 13
  • [30] Java']Java
    不详
    [J]. JOURNAL OF OBJECT-ORIENTED PROGRAMMING, 1996, 9 (06): : 96 - 96
12345