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