GNAT packages in Linux distributions
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 11 May 2010 19:44 Le Tue, 11 May 2010 21:45:45 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > 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 Hey Folks! I'm dreaming! I've just installed the last version of SPARK, started to play a bit with its basic principles on a test package, then, just to see what will happened, turned the package into a generic. And you know what ? Yes, you guess : the SPARK examiner did not returned any error about it and just displayed the message About to call SetPackageIsGeneric P ThePackage P IS GENERIC I though it has simply drop the whole text, so I've introduced an error on purpose in the package, and it has complained about the error (a missing annotation for a procedure declaration), which is the proof that it did not drop the package text. Nice, looks promising. Well, that's just the examiner, that's not all the stuff (which I still need to learn)... anyway, I like that. Hope you will try too I will open a later thread about some SPARK stuffs (for questions, as I'm just beginning with it). P.S. Do not know what implies this âAbout to call SetPackageIsGeneric Pâ, just hope I do not have to bother for the time. -- pragma Asset ? Is that true ? Waaww... great
From: stefan-lucks on 12 May 2010 04:41 On Tue, 11 May 2010, Dmitry A. Kazakov wrote: > On Tue, 11 May 2010 18:05:42 +0200, Yannick Duch�ne (Hibou57) wrote: > > > 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. Actually, there is a difference between partial and total correctness. A program is partially correct, if it produces the correct result in the case it produces any result. A partially correct program may run infinitely or abort with an exception, but when it does neither, you get the specified result. A totally correct program is partially correct *and* terminates in finite time *and* doesn't abort with an unhandled exception. So Eiffel programs seen to be partially correct, but lack any proof of total correctness. Which is OK for some applications. I would expect the autopilot of an airplane to be totally correct -- partial correctness wouldn't be too helpful. But there are plenty of applications, where a partially correct program would be a huge improvement over all the software we are currently using ... BTW, SPARK also only provides partial correctness, but no total correctness. While SPARK allows to prove that no exception is raised (*), it lacks the option to specify (and verify, of course) variants for WHILE-loops (**). Eiffel supports such invariants. So long Stefan P.S.: I have worked a bit with SPARK, and I am currently trying to improve my knowledge about it. While I do prefer static analysis over Eiffels dynamic checking at run time, I still think Eiffel's approach has its place. The constraints of SPARK as a programming language are severe. (For me, the worst is the prohibition of recursive subprograms.) ------ (*) Actually, as much as I understand SPARK, it doesn't allow to prove that the absence of Storage_Error. For that purpose, one needs an additional compiler-specific tool. (**) I just read that the most recent version of SPARK is able to deal with generics. Great! Maybe, SPARK has also recently learned how to specify and prove loop variants? -- ------ 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: Mark Lorenzen on 12 May 2010 08:12 On 12 Maj, 01:44, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Hey Folks! I'm dreaming! > > I've just installed the last version of SPARK, started to play a bit with > its basic principles on a test package, then, just to see what will > happened, turned the package into a generic. And you know what ? Yes, you > guess : the SPARK examiner did not returned any error about it and just > displayed the message > > About to call SetPackageIsGeneric P > ThePackage P > IS GENERIC > > I though it has simply drop the whole text, so I've introduced an error on > purpose in the package, and it has complained about the error (a missing > annotation for a procedure declaration), which is the proof that it did > not drop the package text. > > Nice, looks promising. The planned support for generics was announced at the "Introducing SPARK 9.0" webinar, see http://www.adacore.com/home/products/gnatpro/webinars/ and click "Introducing SPARK 9.0". The announcement is at 25:30 to 26:50. - Mark L
From: Yannick Duchêne (Hibou57) on 12 May 2010 10:52 Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks(a)see-the.signature> a écrit: > it lacks the option to specify (and verify, of course) variants for > WHILE-loops (**). Eiffel supports such > invariants. I was to ask you if you were really sure, ... you've already requested for more comments in the P.S., so may not give me an answer. Well, you may also see a loop as an abstraction surrounded by pre and post and requires the previous state in some the same as the new one after each iteration (just a beginner's two cents idea) > P.S.: I have worked a bit with SPARK, and I am currently trying to > improve my knowledge about it. While I do prefer static analysis > over Eiffels dynamic checking at run time, I still think Eiffel's > approach has its place. The constraints of SPARK as a programming > language are severe. (For me, the worst is the prohibition of > recursive subprograms.) I'm just starting with SPARK, so I may be wrong : it seems to me recursion is allowed if the stack usage is bounded (keep in mind I may be wrong). -- pragma Asset ? Is that true ? Waaww... great
From: Yannick Duchêne (Hibou57) on 12 May 2010 10:55
Le Wed, 12 May 2010 14:12:31 +0200, Mark Lorenzen <mark.lorenzen(a)gmail.com> a écrit: > The planned support for generics was announced at the "Introducing > SPARK 9.0" webinar, see > http://www.adacore.com/home/products/gnatpro/webinars/ > and click "Introducing SPARK 9.0". The announcement is at 25:30 to > 26:50. > > - Mark L I've posted a planned to support generic previously I've discovered support seems to be already there. Your link (interesting) shows it recent. Thanks for the news. -- pragma Asset ? Is that true ? Waaww... great |