|08/27/01||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.|
|08/27/01||114||Lemma 8.1.2: Replace a by alpha.|
|08/27/01||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.|
|08/27/01||152||Figure 10.2: Replace pushFrame(c/<clinit>()) by pushFrame(c/<clinit>(),()).|
|08/24/01||162||Definition of execVME (case Checkcast): Replace 0 by null.|
|08/24/01||274||line 6: Replace seven by eight.|
|07/30/01||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.
|07/30/01||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.
|07/04/01||236||Line 3 in first paragraph: Replace wich by which.|
|07/04/01||267||Proof of Theorem 16.5.1: Replace succs by succ.|
|07/04/01||268||Proof of Theorem 16.5.1: Replace succs by succ.|
|07/03/01||284||Definition of propagateVME (case Jsr(s)): Replace forall by forall seq (execute the rules sequentially).|
|07/03/01||276||Definition of verifySchemeI: Execute changed(pc) := undef and propagateVM(code,succ,pc) sequentially.|
|07/03/01||276||Definition of propagateVMI: Replace forall by forall-seq (execute the rules sequentially).|
|06/25/01||263||Proof of Corollay 16.5.1 (it should be): By Lemma 16.5.10, endgamma is reachable from beggamma via a path ...|
|06/25/01||271||Exercise 16.5.2: Replace regTi by opdTi.|
|06/20/01||256||Line 9 in second paragraph:
Replace V(alpha) = InInit by V(alpha) = [InInit].
Remark: V(alpha) is a list (by definition).
|06/20/01||257||Figure 16.23, S(exp;): Replace [V(beta)] by V(beta).|
|06/20/01||259||Figure 16.27, S(throw exp): Replace [V(beta)] by V(beta).|
|06/20/01||260||Figure 16.28, S(return exp): Replace E(exp) and [V(beta)] by E(exp,[ ]) and V(beta), respectively.|
|06/15/01||210||Definition of defensiveSchemeI: Replace instr by code(pc).|
|06/15/01||212||Definition of checkI: Parameter pc not necessary.|
|06/15/01||214||Definition of checkC: Parameter pc not necessary.|
|06/15/01||218||Definition of checkO: Parameter pc not necessary.|
|06/15/01||220||Definition of checkE: Parameter pc not necessary.|
|06/15/01||236||Line before Lemma 16.2.1: Parameter pc for checkE not necessary.|
|06/15/01||240||Line 8: Parameter pc for checkE not necessary.|
|06/15/01||276||Definition of verifySchemeI: Parameter pc for check not necessary.|
|06/15/01||278||Second paragraph in proof for Theorem 17.1.2: Parameter pc for check not necessary.|
|06/12/01||228||Line 1: Replace Throw by Athrow.|
|06/12/01||237||Definition 16.3.1: Replace Throw by Athrow.|
|06/12/01||239||T7 e: Font of the second l should be equal to the first l (TeX symbol \ell).|
|05/31/01||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*).
|05/25/01||115||Definition 8.1.8 (item 4): Replace lookup(A,Thread/run())=C by lookup(A,Runnable/run())=C.|
|05/25/01||120||Exercise 8.2.4: By replacing the while condition i!=0 by i>=0, we make the exercise more reasonable.|
|05/25/01||122||Section 8.3: Replace type(alpha) by T(alpha). [4 times].|
|05/25/01||130||(chain 1): Replace type(beta) by T(beta).|
|05/23/01||119||Definition 8.2.3 (item 2): Replace throws exp by throw exp.|
|05/18/01||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().|
|05/10/01||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