GNAT packages in Linux distributions
in [ADA]
|
From: Pascal Obry on 11 May 2010 12:09 Le 11/05/2010 18:09, Pascal Obry a �crit : > Le 11/05/2010 18:05, Yannick Duch�ne (Hibou57) a �crit : >> While they can be compared in some way, there is indeed a big difference >> : Eiffel is runtime oriented, SPARK is static analysis oriented. > > Right, I've worked on both languages SPARK and Eiffel. I meant "I've worked with both..." -- --|------------------------------------------------------ --| 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: stefan-lucks on 11 May 2010 13:08 On Tue, 11 May 2010, Pascal Obry wrote: > Le 11/05/2010 18:09, Pascal Obry a �crit : > > Le 11/05/2010 18:05, Yannick Duch�ne (Hibou57) a �crit : > >> While they can be compared in some way, there is indeed a big difference > >> : Eiffel is runtime oriented, SPARK is static analysis oriented. > > > > Right, I've worked on both languages SPARK and Eiffel. > > I meant "I've worked with both..." I am curious. Would you be willing to share some of your experience and tell us about the advantages and disadvantages of both approaches? 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: Yannick Duchêne (Hibou57) on 11 May 2010 12:23 Le Tue, 11 May 2010 18:09:14 +0200, Pascal Obry <pascal(a)obry.net> a écrit: > Le 11/05/2010 18:05, Yannick Duchêne (Hibou57) a écrit : >> While they can be compared in some way, there is indeed a big difference >> : Eiffel is runtime oriented, SPARK is static analysis oriented. > > Right, I've worked on both languages SPARK and Eiffel. If you like anecdotes, just note that Design by Contract, which is one target of SPARK, is a registered trade-mark of Bertrand Meyer, the author of Eiffel as you know ;) (personal opinion : an occasion to say I feel this kind of mark registration is an abuse) -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 11 May 2010 12:39 Le Tue, 11 May 2010 19:08:16 +0200, <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? > > Stefan Well, as noted above, Eiffel is far more popular than SPARK, and there is a reason for that : as Eiffel is runtime oriented, it is less strict than SPARK, which is static analysis oriented. Let say there is the same differences between SPARK and Eiffel than the ones you may have between typed and non-typed language. A non-type language does not require you to validate any thing until runtime, and runtime (and to reach a specific branch, which is important to note) to raise an error (providing it is as least able to raise an error in such circumstance). The same comment apply with SPARK vs Eiffel : Eiffel allow you to run a program without any other requirement, it just interpret the pre- and post- and invariant conditions you've written (Yes, although it is a compiled language, this features of Design by Contract are still interpreted in Eiffel, just like pragma Assertion are in Ada by the way).. Hey... you know, untyped language seems far easier at first glance : you write, you run, it crash... you modify some this-and-that, you run again... it don't crash (I mean you don't when and why it will crash the next time, which may wait for some weeks, months or year, who know ...) Just think about the amount of time you may spent before making a program proof with SPARK, and compare that to the Eiffel way, where you will never know your implementation is wrong (so you will not have reason to be disappointed, although things are still wrong what ever is your feeling about it). If you want to enjoy your language, Eiffel is probably the best. .... hmmmm.... after some though, this may depends on what to âenjoyâ requires to you ; so the above sentence may or may not be true finally. Seriously, given two languages, one which allow you to run you application the sooner, which one do you think many body will prefer ? ;) Guess what is most famous and popular : JavaScript or Ada ? I think this draw the big line. 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 complex application. The answer is Yes, as you are not required to validate all of your application with SPARK, and you can validate some part of it. Think about SPARK as a step above typing. Typing just make proofs on components of your application, not on the application. SPARK may be used the same way, to make proofs on some component as well... and it is able to make proofs which cannot be expressed with type definitions. -- pragma Asset ? Is that true ? Waaww... great
From: J-P. Rosen on 11 May 2010 12:41
Yannick Duch�ne (Hibou57) a �crit : > Le Tue, 11 May 2010 18:09:14 +0200, Pascal Obry <pascal(a)obry.net> a �crit: > >> Le 11/05/2010 18:05, Yannick Duch�ne (Hibou57) a �crit : >>> While they can be compared in some way, there is indeed a big difference >>> : Eiffel is runtime oriented, SPARK is static analysis oriented. >> >> Right, I've worked on both languages SPARK and Eiffel. > > If you like anecdotes, [...] > And another anecdote is that Eiffel was designed by Bertrand Meyer when he worked for the research center of EdF (french electricity company), where Pascal is currently working too... -- --------------------------------------------------------- J-P. Rosen (rosen(a)adalog.fr) Visit Adalog's web site at http://www.adalog.fr |