GNAT packages in Linux distributions
in [ADA]
|
From: Dmitry A. Kazakov on 11 May 2010 12:45 On Tue, 11 May 2010 18:05:42 +0200, Yannick Duch�ne (Hibou57) wrote: > Le Tue, 11 May 2010 17:46:58 +0200, Pascal Obry <pascal(a)obry.net> a �crit: > >> Le 11/05/2010 09:39, Dmitry A. Kazakov a �crit : >>> I am not. Eiffel does it wrong. SPARK does it right. >> >> Eiffel and SPARK are completely different beasts, I do not see how you >> can compare them. >> > Can be compared in their attempt to make proofs or to draw a path to it. > But Eiffel's concepts are mostly a kind of debugging or runtime exception > oriented, and you are right if you were to point that Eiffel is not to do > static inference. Because it does not include exceptions in the contract, which is obviously wrong. > While they can be compared in some way, there is indeed a big difference : > Eiffel is runtime oriented, SPARK is static analysis oriented. A proof of correctness cannot be run-time. Incorrectness need no proof. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Pascal Obry on 11 May 2010 13:35 Le 11/05/2010 19:08, stefan-lucks(a)see-the.signature a �crit : > I am curious. Would you be willing to share some of your experience and > tell us about the advantages and disadvantages of both approaches? Yannick has answered this question now. I would just add that SPARK is *hard* (very hard) to program but at the end it gives you a proof just by looking at your code. Eiffel in contrast is far more easier to program, but well the constraints (pre/post conditions, invariants) are only checked at runtime. Problems will be found when this part of the code is run. I cannot say I prefer one or the other. I've stopped programming in Eiffel long time ago now. Both are targeting different level of safety and security to me. I can say that my second best/preferred language is Eiffel. It is a clean language, well designed that encourage good programming. Pascal. -- --|------------------------------------------------------ --| Pascal Obry Team-Ada Member --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE --|------------------------------------------------------ --| http://www.obry.net - http://v2p.fr.eu.org --| "The best way to travel is by means of imagination" --| --| gpg --keyserver keys.gnupg.net --recv-key F949BD3B
From: Yannick Duchêne (Hibou57) on 11 May 2010 14:06 Le Tue, 11 May 2010 19:35:43 +0200, Pascal Obry <pascal(a)obry.net> a écrit: > Eiffel in contrast is far more easier to program, but well the > constraints (pre/post conditions, invariants) are only checked at > runtime. Problems will be found when this part of the code is run. > > I cannot say I prefer one or the other. I've stopped programming in > Eiffel long time ago now. Both are targeting different level of safety > and security to me. > > I can say that my second best/preferred language is Eiffel. It is a > clean language, well designed that encourage good programming. > > Pascal. I remember I had the idea to leave Eiffel for one main first reason : its lack in the basic types area. The set of basic type was (I say âwasâ, as I don't know if the Eiffel ISO standard has evolved since) too much restricted and there was no way to create proper new ones. There was a good reason to that : Eiffel is far from low level ; it is unlikely you will be able to conceive a device driver with Eiffel. I'm not pointing that to say Eiffel is not nice because of that exact point ; this is just a matter of requirement. That said, as long as there are some fault tolerance and as long as low level is not involved, it is a nice one, which as you said, may give you some good ideas and good inspirations ;) Further more, there was a plan from Bertrand Meyer (do not have the reference any more, sorry) to promote Eiffel as a language for the web platform (I mean client side, that is, browsers). If this would have been a success, we may actually have Eiffel instead of JavaScript for web applications. Eiffel would have been well suited to this area : semantic favorable to interpretation and execution of remote stuff (no pointers to method, just references, which can mean Anything on the other side), clean enough, *accessible enough*, promoting some good though for peoples willing to receive these. -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 11 May 2010 15:21 Le Tue, 11 May 2010 18:45:14 +0200, Dmitry A. Kazakov <mailbox(a)dmitry-kazakov.de> a écrit: > A proof of correctness cannot be run-time. Incorrectness need no proof.. I guess you will not like it, however, here is my disclaimer : there may be some levels of correctness. A well written Eiffel application is more near to be correct than let say an XXXXX (I prefer to not give any names) one. Yes, it will not be 100% logically-proven. That said, isn't let say 40% trustable better than 0% or even less ? Even SPARK has different levels of checking (at least two ones) Obviously, Eiffel is not a theorem prover, while it still comes with a philosophy. P.S. Don't be afraid, you next plane or train will not be Eiffel powered anyway, there is no need to be afraid about its lacks, compared to SPARK, which is not a tiny thing. -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 11 May 2010 15:45
Le Tue, 11 May 2010 18:39:52 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > TBH, there is also some important restriction which SPARK applies to > what you may use with Ada : you will not be allowed to use generics and > polymorphic dispatching as two examples. Why ? Just because SPARK cannot > make some proof based on these materials. So is SPARK useful for more This limitation (generics) may not be always true, as it seems there are some plans to change it : AdaCore and Praxis are working toward this. Interested parties may have a look at this quick presentation : http://mpri.master.univ-paris7.fr/stages-2010/20091104-154948/sujet-containers.pdf In the area of logic proof of program, this, is also interesting : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-November/001525.html And even more the reply : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-November/001532.html This latter highlight what SPARK is with a comparison to Frama-C and its ACSL (yep, it stands for ANSI C Specification Langage). -- pragma Asset ? Is that true ? Waaww... great |