[Prev][Next][Index][Thread]

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
 
=====================================================================
Sophia Drossopoulou, from Imperial College London, 
                                      perm email:    sd@doc.ic.ac.uk 
currently visiting Prof. Mariangiola Dezani-Ciancaglini, Univ. Torino
		                      curr email: sophia@di.unito.it 
=====================================================================