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 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!news4.google.com!news.glorb.com!newsfeed00.sul.t-online.de!t-online.de!inka.de!rz.uni-karlsruhe.de!news.belwue.de!LF.net!news.enyo.de!not-for-mail From: Florian Weimer Newsgroups: comp.lang.ada Subject: Re: Type safety on wikipedia Date: Thu, 26 Jan 2006 20:07:50 +0100 Message-ID: <87fynaajuh.fsf@mid.deneb.enyo.de> References: <1138260496.230283.147640@g43g2000cwa.googlegroups.com> <1138283608.433842.76060@z14g2000cwz.googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: albireo.enyo.de 1138302472 11902 212.9.189.177 (26 Jan 2006 19:07:52 GMT) X-Complaints-To: Cancel-Lock: sha1:6DqeC3795chTUv+f57BBpxJTgmU= Xref: g2news1.google.com comp.lang.ada:2662 Date: 2006-01-26T20:07:50+01:00 List-Id: > 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.