Java and the Java Virtual Machine (R. Stärk, J. Schmid, E. Börger)

Errata and remarks for Jbook

Remarks and corrections are listed by increasing page numbers. Take a look at this page for the updates listed in chronological order.
Page Description
52 Constraint 4.1.6 (item 9): The body of the method is the semicolon if, and only if, the method is abstract or native.
103 In the definition of start(ref), the expression lookup(classOf(q),Thread/run())/run() should be replaced by lookup(classOf(q),Runnable/run())/run().
105 In the definition of wait(ref), the interruptedFlag(thread) should be checked. If it is True, then an InterrupedException should be thrown and the flag should be cleared. The IllegalMonitorStateException has priority over the InterrupedException.
114 Lemma 8.1.2: Replace a by alpha.
115 Definition 8.1.8 (item 4): Replace lookup(A,Thread/run())=C by lookup(A,Runnable/run())=C.
119 Definition 8.2.3 (item 2): Replace throws exp by throw exp.
120 Exercise 8.2.4: By replacing the while condition i!=0 by i>=0, we make the exercise more reasonable.
122 Section 8.3: Replace type(alpha) by T(alpha). [4 times].
129 Theorem 8.4.1 (Java is type safe): The invariant (def5) has to be changed to
If restbody*/alpha = Break(l), then break(alpha,l) is contained in dom(locals*).
130 (chain 1): Replace type(beta) by T(beta).
140 Fifth paragraph: We denote by JVMS(p,ws) the sequence of words corresponding to the application of the primitive operator p to the argument sequence ws according to the JVM specification.
145 Exchange stm1 and stm2 in:
If the result of the test is True (different from integer 0), then control jumps to the code of stm2. Otherwise, stm1 is executed.
152 Figure 10.2: Replace pushFrame(c/<clinit>()) by pushFrame(c/<clinit>(),()).
162 Definition of execVME (case Checkcast): Replace 0 by null.
210 Definition of defensiveSchemeI: Replace instr by code(pc).
212 Definition of checkI: Parameter pc not necessary.
214 Definition of checkC: Parameter pc not necessary.
218 Definition of checkO: Parameter pc not necessary.
220 Definition of checkE: Parameter pc not necessary.
228 Line 1: Replace Throw by Athrow.
229 Why sets of reference types?
Sun's JDK 1.2 verifier does not reject the bytecode. Instead it inserts an additional run-time check for methods with arguments of interface type. Hence, the compatibility of method arguments has to be checked at run-time in contradiction to the JVM specification
Sun's JDK 1.2 verifier does not reject the bytecode. Instead it inserts an additional run-time check for invocations of interface methods. According to the JVM specification an IncompatibleClassChangeError is thrown at run-time, if the target object of an interface method invocation does not implement the interface.
236 Line before Lemma 16.2.1: Parameter pc for checkE not necessary.
236 Line 3 in first paragraph: Replace wich by which.
237 Definition 16.3.1: Replace Throw by Athrow.
239 T7 e: Font of the second l should be equal to the first l (TeX symbol \ell).
240 Line 8: Parameter pc for checkE not necessary.
256 Line 9 in second paragraph: Replace V(alpha) = InInit by V(alpha) = [InInit].
Remark: V(alpha) is a list (by definition).
257 Figure 16.23, S(exp;): Replace [V(beta)] by V(beta).
259 Figure 16.27, S(throw exp): Replace [V(beta)] by V(beta).
260 Figure 16.28, S(return exp): Replace E(exp) and [V(beta)] by E(exp,[ ]) and V(beta), respectively.
263 Proof of Corollay 16.5.1 (it should be): By Lemma 16.5.10, endgamma is reachable from beggamma via a path ...
267 Proof of Theorem 16.5.1: Replace succs by succ.
268 Proof of Theorem 16.5.1: Replace succs by succ.
271 Exercise 16.5.2: Replace regTi by opdTi.
274 line 6: Replace seven by eight.
276 Definition of verifySchemeI: Parameter pc for check not necessary.
276 Definition of verifySchemeI: Execute changed(pc) := undef and propagateVM(code,succ,pc) sequentially.
276 Definition of propagateVMI: Replace forall by forall-seq (execute the rules sequentially).
278 Second paragraph in proof for Theorem 17.1.2: Parameter pc for check not necessary.
284 Definition of propagateVME (case Jsr(s)): Replace forall by forall seq (execute the rules sequentially).
332 By replacing the two occurrences of IndexOutOfBoundsException by ArrayIndexOutOfBoundsException we can reflect the change from JLS 1.0 to JLS 2.0.


ETH Home August 2001
ETH Logo