Re: Type soundness issues in Java
More on the claim I suggested two days ago -- I probably mis-used the terms
(did not have a Java spec near at hand):
Consider a program P_0 which contains several handlers for Errors
(which it does not have to do, but it may do if the programmer
wants to do it). Also, execution of P_0 will throw Errors related
to verification and loading.
Now consider that P_0 runs on different implementations. It may
have different effects, or return with different errors.
Namely, consider that P_0 runs on implementation Impl_1. It throws
error Error_1, which is caught by some handler H_1 in program P_0. Then
P_0 might return, say value v_1.
Alternatively, if P_0 runs on implementation Impl_2, it may throw
error Error_2, which is caught by another handler H_2 in program P_0. Then
P_0 might return, say value v_2.
Next, if P_0 runs on implementation Impl_3, it may throw
error Error_3, which is not caught, so P_0 terminates reporting Error_3.
Finally, if P_0 runs on implementation Impl_4, it may throw
error Error_4, which is not caught, so P_0 terminates reporting Error_4.
I find the fact that different errors may be reported (Impl_3 and Impl_4)
not that exciting. But the fact that handlers may catch the errors, and so
return different values seems more alarming to me.
Note however, that the above does not affect type soundness, because the
different values will have the same type.
>"Sophia Drossopoulou(Osp. Dezani)" wrote:
>> Could we replace the above claim by the following, weaker one?
>> Let us consider an eager implementation EI (eager loading and verification).
>> Then, every program that executes on EI without throwing an unchecked
>> exception should have the same behaviour on every other implementation.
>> On the other hand, a program that throws an unchecked exception on some
>> implementation will also throw an unchecked exception (although not
>> necessarily the same one) on EI.
>> The applicability of the above claim would be severely reduced by the
>> fact that we can handle exceptions in Java. Therefore, the behaviour
>> of a program that throws an unchecked exception AND handles it cannot
>> be compared to the behaviour of the same program on EI. The two
>> implementations could even return different values, or one could
>> terminate abnormally and the other could handle the exception and
>> terminate abnormally.
"Zhenyu Qian" wrote:
>Java and JVM Specs seem to require that all "Throwable" objects that may be thrown
>by JVM, BC verifier and class loaders are "Error" objects, not "Exception" objects
>("Error" and "Exception" are subclasses of "Throwable"). "Error" objects need not be
>cought by Java programs. (Of course, this does not prevent the user to write Java
>programs to catch "Error" objects.)
I think I used the wrong term (did not have a Java spec near at hand
and got slightly misunderstood). Above, I tried to clarify my meaning.
Sophia Drossopoulou, from Imperial College London,
perm email: email@example.com
currently visiting Prof. Mariangiola Dezani-Ciancaglini, Univ. Torino
curr email: firstname.lastname@example.org