Dynamic semantics of Java']Java bytecode

被引：6
|
作者：
Bertelsen, P [1 ]
机构：
[1] Royal Vet & Agr Univ, Dept Math & Phys, Copenhagen, Denmark
来源：
FUTURE GENERATION COMPUTER SYSTEMS | 2000年 / 16卷 / 07期
关键词：
!text type='Java']Java[!/text; !text type='Java']Java[!/text] Virtual Machine; formal specification; semantics;
D O I：
10.1016/S0167-739X(99)00094-1
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We give a formal specification of the dynamic semantics of Java bytecode, in the form of an operational semantics for the Java Virtual Machine (JVM). For each JVM instruction we give a rule describing the instruction's effect on the machine state and the conditions under which the instruction will execute without error. This paper outlines the formalization of the JVM machine state and illustrates our approach for a few select JVM instructions. Our full specification, covering the entire JVM instruction set except for synchronization instructions, is available in the work of Bertelsen (Semantics of Java byte code, Technical Report, Department of Mathematics and Physics, Royal Veterinary and Agricultural University, Copenhagen, Denmark, April 1997). (C) 2000 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：841 / 850
页数：10
相关论文
共 50 条
  • [1] Extending operational semantics of the Java']Java bytecode
    Czarnik, Patryk
    Schubert, Aleksy
    [J]. TRUSTWORTHY GLOBAL COMPUTING, 2008, 4912 : 57 - 72
  • [2] Altering Java']Java semantics via bytecode manipulation
    Tanter, E
    Ségura-Devillechaise, M
    Noyé, J
    Piquer, J
    [J]. GENERATIVE PROGRAMMING AND COMPONENT ENGINEERING 2002, PROCEEDINGS, 2002, 2487 : 283 - 298
  • [3] Dynamic slicing on Java']Java bytecode traces
    Wang, Tao
    Roychoudhury, Abhik
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2008, 30 (02):
  • [4] Dynamic slicing of Java']Java bytecode programs
    Szegedi, A
    Gyimóthy, T
    [J]. FIFTH IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2005, : 35 - 44
  • [5] A Java']Java processor architecture with bytecode folding and dynamic scheduling
    El-Kharashi, MW
    Elguibaly, F
    Li, KF
    [J]. 2001 IEEE PACIFIC RIM CONFERENCE ON COMMUNICATIONS, COMPUTERS AND SIGNAL PROCESSING, VOLS I AND II, CONFERENCE PROCEEDINGS, 2001, : 307 - 310
  • [6] An Evaluation of Dynamic Java']Java Bytecode Software Watermarking Algorithms
    Kumar, Krishan
    Kehar, Viney
    Kaur, Prabhpreet
    [J]. INTERNATIONAL JOURNAL OF SECURITY AND ITS APPLICATIONS, 2016, 10 (07): : 147 - 156
  • [7] Java']Java bytecode verification
    Nipkow, T
    [J]. JOURNAL OF AUTOMATED REASONING, 2003, 30 (3-4) : 233 - 233
  • [8] Java']Java bytecode optimizations
    Lambright, HD
    [J]. IEEE COMPCON 97, PROCEEDINGS, 1997, : 206 - 210
  • [9] A Java']Java Bytecode Formalisation
    Czarnik, Patryk
    Chrzaszcz, Jacek
    Schubert, Aleksy
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, (VSTTE 2018), 2018, 11294 : 135 - 154
  • [10] Dynamic instrumentation of distributed Java']Java applications using bytecode modifications
    Funika, Wlodzimierz
    Swierszcz, Pawel
    [J]. COMPUTATIONAL SCIENCE - ICCS 2006, PT 2, PROCEEDINGS, 2006, 3992 : 534 - 541
12345