GNAT packages in Linux distributions
in [ADA]
|
From: stefan-lucks on 26 May 2010 04:38 On Tue, 25 May 2010, Yannick Duch�ne (Hibou57) wrote: > There is a major difference : Eiffel's pre/cond on methods are inherited by > derived class. With C, or even with Ada' pragma Assert, this have to be done > manually. > > Side note: I'm not talking about pre/cond in Ada 2012/2015, which will be > closer to that of Eiffel. However, as SPARK already has this and do it better > from my point of view (because of static checking and proofs), I am not > waiting for Ada 2012/2015 for that. Don't underestmate Ada2012 (or Eiffel, for that point): Being able to natively *express* contracts in a programming language itself, instead of using some more or less informal comments, as can be done in any other languages is a quantum leap. This is regardless of any checking! (Not that I disagree with you: Static checking, as provided by SPARK, is a BIG THING by itself.) Defining a derived language which uses the mother language's comments for an "annotation" syntax (like SPARK, some Java-derivatives, ...) is the poor man's (or poor woman's) approach. I would really hope that SPARK will soon after the appearance of Ada 2012 support the new contract syntax. Stefan -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------
From: Dmitry A. Kazakov on 26 May 2010 03:55 On Tue, 25 May 2010 22:45:31 +0200, Yannick Duch�ne (Hibou57) wrote: > Le Wed, 12 May 2010 19:24:11 +0200, Dmitry A. Kazakov > <mailbox(a)dmitry-kazakov.de> a �crit: >> Yes, it is better but that is not the point. Which is there is no >> substantial difference between Eiffel precondition and C's if statement >> beyond syntax sugar, and that if-statement is less misleading. > There is a major difference : Eiffel's pre/cond on methods are inherited > by derived class. No, because the inheritance generates code. It is still code, rather than error messages. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Yannick Duchêne (Hibou57) on 26 May 2010 04:01 Le Wed, 26 May 2010 10:38:20 +0200, <stefan-lucks(a)see-the.signature> a écrit: > I would really hope that SPARK will > soon after the appearance of Ada 2012 support the new contract syntax. A question I have in mind indeed : will SPARK evolve to take these future pre/post into account ? -- There is even better than a pragma Assert: a SPARK --# check.
From: Yannick Duchêne (Hibou57) on 26 May 2010 07:25 Le Wed, 26 May 2010 10:38:20 +0200, <stefan-lucks(a)see-the.signature> a écrit: > Defining a derived language which uses the mother language's comments for > an "annotation" syntax (like SPARK, some Java-derivatives, About this comparison to Java : JML (Java Modeling Language) which is the corresponding DbC (Design By Contract) language for Java, is not aimed at static analysis, it creates conditions which are checked at runtime only (as far as I've understood). So there is no way to compare JML and SPARK.. Please, can you tell me more about what âannotationsâ implies to you ? To give a small talk, I would just say that if it either appears in comment or in plain language source, I do not see a difference. -- There is even better than a pragma Assert: a SPARK --# check.
From: stefan-lucks on 26 May 2010 09:02
On Wed, 26 May 2010, Yannick Duch�ne (Hibou57) wrote: > Please, can you tell me more about what �annotations� implies to you ? Annotations are an addition to the original language. Annotations are typically "hidden" in comments (from the viewpoint of the original language). This is in constrast to contracts defined as a part of the language itself. (Technically, the language with the annotations makes a new language ... but there is a gap between the normal part of the language, and the comment-like annotations. > To give a small talk, I would just say that if it either appears in > comment or in plain language source, I do not see a difference. I am a university teacher. For me, it makes quite a difference if I either explain studens one coherent language where contracts are an integral part of (like Eiffel), or one programming langugage plus an additional language for the annotations. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------ |