From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,80bc3e0698be468f
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news2.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: "Alex R. Mosteo" <devnull@mailinator.com>
Newsgroups: comp.lang.ada
Subject: Re: Type safety on wikipedia
Date: Fri, 27 Jan 2006 12:34:29 +0100
Message-ID: <43DA0545.8030904@mailinator.com>
References: <1138260496.230283.147640@g43g2000cwa.googlegroups.com>
	<1138283608.433842.76060@z14g2000cwz.googlegroups.com>
 <87fynaajuh.fsf@mid.deneb.enyo.de>
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: individual.net zVWjc0DP8gofpUFrYuB2AQpno4iE3ykD76Gj3u7L/k3S7yWEM=
User-Agent: Mozilla Thunderbird 1.0.7 (X11/20051013)
X-Accept-Language: en-us, en
In-Reply-To: <87fynaajuh.fsf@mid.deneb.enyo.de>
Xref: g2news1.google.com comp.lang.ada:2674
Date: 2006-01-27T12:34:29+01:00
List-Id: <comp.lang.ada>

Florian Weimer wrote:
>>Even with unchecked conversion Ada has the 'Valid attribute, allowing
>>the programmer to determine if the result of an unchecked conversion is
>>a valid value.
> 
> 
> Only in very limited cases.
> 
> 
>>I do not see how Unchecked_Deallocation interferes with type safety.
> 
> 
> The following is just a rough sketch, but maybe it helps to clarify
> the terms.
> 
> A type system gives you a subset of all expressions which are
> well-typed (in Ada, 1 + 1 is well-typed, but 1.0 + 1 is not).
> 
> A type-safe language has a type system with these two properties: any
> well-typed expression which is not a value can be reduced to a simpler
> expression, according to a set of run-time evaluation rules (which
> define the semantics of the language) -- and these simplification
> steps preserve the well-typedness of expressions.
> 
> (Of course, considerable notational overhead is needed to apply this
> definitions in a rigorous manner to real-world programming languages.)
> 
> Now, suppose that X is a pool-specific access value for some type T,
> and Free is a corresponding instance of Ada.Unchecked_Deallocation.
> Suppose that
> 
> 
>    Free (X);
> 
> has just been exected.  Suppose the next thing to be evaluated is
> 
>    declare
>       Y : T := X.all;
>    begin
>       ...
> 
> Now X.all is not a value, so it has to reduce (at run-time) to some
> other expression.  But the language definition explicitly tells you
> that no such rule exists.  Therefore, the first rule I mentioned is
> violated, and Ada with Ada.Unchecked_Deallocation is not type-safe.

Thanks for your effort in making us understand. However, there's still 
something fundamental that I'm not grasping.

According to the current Wikipedia article, Java is believed to be type 
safe. However, one can have null pointers in Java. For example:

public class Test {
	public static void main (String args[]) {
		Integer x = new Integer (5);
		Integer y = null;
		
		System.out.println ("X + Y: " + (x + y));
	}
}

will compile without warnings with latest JDK1.5 and run as:

$ java Test
X: 5
Exception in thread "main" java.lang.NullPointerException
         at Test.main(Test.java:7)

This means that Java has explicit rules for when this happens that 
differ from those in Ada? Since Ada also detects null pointer usage, and 
per your example it makes Ada type unsafe.

Conversely, I understand that evaluations that yield out-of-range values 
don't make a language type-unsafe because these cases have well-defined 
rules of behavior.

Maybe I should go now to read the original paper linked from the wikipedia.