|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
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