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: a07f3367d7,23c0de5a42cf667e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 Path: g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!fdn.fr!gegeweb.org!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: GNAT packages in Linux distributions Date: Wed, 12 May 2010 18:06:16 +0200 Organization: Ada At Home Message-ID: References: <87mxw9x7no.fsf@ludovic-brenta.org> <16bz9kvbqa8y9$.155ntpwpwl29d.dlg@40tude.net> <4be97bea$0$2966$ba4acef3@reader.news.orange.fr> <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> NNTP-Posting-Host: FD8vExnEy5iRSNWAUP6U/Q.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 User-Agent: Opera Mail/10.53 (Win32) Xref: g2news2.google.com comp.lang.ada:11559 Date: 2010-05-12T18:06:16+02:00 List-Id: Le Wed, 12 May 2010 17:37:44 +0200, Dmitry A. Kazakov = a =C3=A9crit: > Any program is partially correct, if otherwise has not been observed. = I > fail to see how Eiffel is different from C or Assembler in that respec= t. If Eiffel was the same as C or assembly, why would Meyer have created it= = and why people seeking for safety would be interested in this one ? OK, the latter assertion is not proof of anything, and I may just be = talking about people who are wrong. Go further : look at Eiffel's syntax and semantic associated to each = syntactic elements and compare that to what's provided with C (by the wa= y, = there exist formal specifications for C as well, I mean ACSL previously = = presented) or assembly. Can't you see something different ? There is at least, and this is not subjective, two areas in which it = differs : expression and runtime-check. Well, I've noted you do not like runtime-check because it is not [formal= ] = proof of anything, but no one said it is formal proof, this is just bett= er = to catch error the sooner and understand why this was an error. This is = = already the purpose of exceptions, and Eiffel's formalism helps in that = = area... because it comes with a formalization. About expression now, although understandability of a source does not = provide proof, this help to at least make partial assertions and discove= r = what's wrong. Obviously, static checker does not even need input which a= re = human readable : does this means we do not need human-readable as a = feature ? A C or assembly designed application is unlikely to raise a run-time = exception when it detect an erroneous runtime condition. It will just = raise exception (or signals) when CPU will be in a critical states as = request for data in an non-existing memory page, as an example. Detectin= g = error at runtime in the program state itself, at an higher level, is = better than this critical kind of CPU level critical state. It is best t= o = face an error like =E2=80=9Cthis class invariant was violated=E2=80=9D t= han =E2=80=9Cthis access = to this memory address failed=E2=80=9D. The purpose of Eiffel is to help= to catch = errors at the higher level as possible, thus at a level which is nearer = to = human or proper application functionalities concern. In that way, this i= s = a step toward abstraction and formal specification. This is not, this is a step toward. Eiffel's not SPARK, there is no doubt about it, and that was previously = = stated, even by Eiffel advocators. However, to say =E2=80=9CC, assembly and Eiffel are all the same and non= e provided = better proof an application may at least run partially good=E2=80=9D is = a lot said = (it is by the way as much true that jocks and teasing kept apart, C is n= ot = the same as assembly) And like Pascal said : =E2=80=9CEiffel is far more easier than SPARK=E2=80= =9D (you cannot = request every one to know SPARK, and you help them when you provide them= = something like Eiffel). Given all that : SPARK is largely known as not being able to handle some= = complex applications, which are yet of every day use (like a web browser= ). = If SPARK cannot handle the whole of these applications, what can we do ?= = Eiffel's approach is a suggested one... This does not statically check = statically, this do it at runtime instead, ... still better than no = abstraction and formalization at all. -- = pragma Asset ? Is that true ? Waaww... great