* GNAT packages in Linux distributions @ 2010-05-09 17:40 Dmitry A. Kazakov 2010-05-09 18:16 ` Ludovic Brenta 2010-05-10 1:40 ` Björn Persson 0 siblings, 2 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-09 17:40 UTC (permalink / raw) For more than a year I has been using either GNAT Pro or GNAT GPL. Recently I installed Fedora and Debian GNAT distributions and discovered that basically all two years old bugs known to me are still present. Some of these bugs were fixed in GNAT GPL 2009, others in GNAT Pro 6.3. So my question is: is there any information or summary on the Web about how Linux distributions are related to AdaCore releases? Or maybe somebody knowledgeable could create and maintain this as a wiki etc. It is important with respect to submitting bug reports. I already did some to Debian. But then I started to discover more and more. Because the bugs I am talking about are known fixed, in my eyes, it does not make any sense to submit them again. (Provided, GNAT will not be developed independently on AdaCore, rather than merely packaged) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 17:40 GNAT packages in Linux distributions Dmitry A. Kazakov @ 2010-05-09 18:16 ` Ludovic Brenta 2010-05-09 19:36 ` Dmitry A. Kazakov 2010-05-10 1:40 ` Björn Persson 1 sibling, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-09 18:16 UTC (permalink / raw) Dmitry A. Kazakov writes on comp.lang.ada: > For more than a year I has been using either GNAT Pro or GNAT > GPL. Recently I installed Fedora and Debian GNAT distributions and > discovered that basically all two years old bugs known to me are still > present. Some of these bugs were fixed in GNAT GPL 2009, others in > GNAT Pro 6.3. > > So my question is: is there any information or summary on the Web > about how Linux distributions are related to AdaCore releases? Or > maybe somebody knowledgeable could create and maintain this as a wiki > etc. http://people.debian.org/~lbrenta/debian-ada-policy.html See section 2.3.4 FSF releases and (now outdated) Appendix B. You will see that the GCC 4.3 you are using is roughly equivalent to GNAT GPL 2007; Debian testing has GCC 4.4 which is roughly equivalent to GNAT GPL 2008. Note that I backport some bug fixes into the Debian version of GCC. > It is important with respect to submitting bug reports. I already did > some to Debian. But then I started to discover more and more. Because > the bugs I am talking about are known fixed, in my eyes, it does not > make any sense to submit them again. (Provided, GNAT will not be > developed independently on AdaCore, rather than merely packaged) "known fixed" to whom? The bug database at AdaCore is private (and with good reason). If you use the FSF version of GNAT, you should use the corresponding bug database: Debian, Fedora or GCC upstream. There are a few contributors external to AdaCore that provide bug fixes into the FSF GCC, sometimes ahead of AdaCore; I normally backport such fixes into the Debian version. Eventually, all bug fixes end up in both GNAT Pro/GPL and in FSF GCC. The keyword is "eventually"; the time lag can be months or years as you noted. -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 18:16 ` Ludovic Brenta @ 2010-05-09 19:36 ` Dmitry A. Kazakov 2010-05-09 21:26 ` Ludovic Brenta 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) 0 siblings, 2 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-09 19:36 UTC (permalink / raw) On Sun, 09 May 2010 20:16:27 +0200, Ludovic Brenta wrote: > Dmitry A. Kazakov writes on comp.lang.ada: >> For more than a year I has been using either GNAT Pro or GNAT >> GPL. Recently I installed Fedora and Debian GNAT distributions and >> discovered that basically all two years old bugs known to me are still >> present. Some of these bugs were fixed in GNAT GPL 2009, others in >> GNAT Pro 6.3. >> >> So my question is: is there any information or summary on the Web >> about how Linux distributions are related to AdaCore releases? Or >> maybe somebody knowledgeable could create and maintain this as a wiki >> etc. > > http://people.debian.org/~lbrenta/debian-ada-policy.html Thanks. I was aware of the document, but didn't read it thoroughly. > See section 2.3.4 FSF releases and (now outdated) Appendix B. You will > see that the GCC 4.3 you are using is roughly equivalent to GNAT GPL > 2007; Debian testing has GCC 4.4 which is roughly equivalent to GNAT GPL > 2008. I.e. 2010 - 2008 = 2 (Fedora - gprbuild, GPS, GNADE ODBC, APQ) 2010 - 2007 = 3 (Debian + gprbuild, GPS, GNADE ODBC, APQ) Right? > Note that I backport some bug fixes into the Debian version of > GCC. Do you have access to AdaCore wavefronts? >> It is important with respect to submitting bug reports. I already did >> some to Debian. But then I started to discover more and more. Because >> the bugs I am talking about are known fixed, in my eyes, it does not >> make any sense to submit them again. (Provided, GNAT will not be >> developed independently on AdaCore, rather than merely packaged) > > "known fixed" to whom? To me. Many I have already forgotten, it is two years since then... > The bug database at AdaCore is private (and with good reason). Whatever reasons might be, they aren't good. (:-() > If you > use the FSF version of GNAT, you should use the corresponding bug > database: Debian, Fedora or GCC upstream. Hmm, that would make sense only for bugs related to the compiler environment, packaging etc. If the bug is a compiler problem, there is no chance it can be fixed unless somebody is working on the compiler itself. For example, there is a bug in assignment of controlled objects. It crashes Debian, leaks in Fedora, fixed in GPL 2009. Should it be reported? Where to? > There are a few contributors external to AdaCore that provide bug fixes > into the FSF GCC, sometimes ahead of AdaCore; I normally backport such > fixes into the Debian version. Eventually, all bug fixes end up in both > GNAT Pro/GPL and in FSF GCC. The keyword is "eventually"; the time lag > can be months or years as you noted. So, when (if) GNAT GPL 2010 come, nothing will sufficiently change for FSF? That is very disappointing. I hoped to jump off the GPL track (not because of the license issue). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 19:36 ` Dmitry A. Kazakov @ 2010-05-09 21:26 ` Ludovic Brenta 2010-05-09 21:34 ` Yannick Duchêne (Hibou57) 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-09 21:26 UTC (permalink / raw) Dmitry A. Kazakov writes: >> http://people.debian.org/~lbrenta/debian-ada-policy.html > > Thanks. I was aware of the document, but didn't read it thoroughly. > >> See section 2.3.4 FSF releases and (now outdated) Appendix B. You will >> see that the GCC 4.3 you are using is roughly equivalent to GNAT GPL >> 2007; Debian testing has GCC 4.4 which is roughly equivalent to GNAT GPL >> 2008. > > I.e. > > 2010 - 2008 = 2 (Fedora - gprbuild, GPS, GNADE ODBC, APQ) > 2010 - 2007 = 3 (Debian + gprbuild, GPS, GNADE ODBC, APQ) > > Right? Not entirely; you should qualify which version of Debian or Fedora you are talking about: 2010 - 2008 = 2 (Fedora ?? - gprbuild, GPS, GNADE ODBC, APQ) 2010 - 2007 = 3 (Debian 5.0 - gprbuild, + GPS, GNADE ODBC, - APQ) 2010 - 2008 = 2 (Debian 6.0 + gprbuild, GPS, GNADE ODBC, APQ) >> Note that I backport some bug fixes into the Debian version of >> GCC. > > Do you have access to AdaCore wavefronts? Not in my capacity as an unpaid, unsupported volunteer. > To me. Many I have already forgotten, it is two years since then... > >> The bug database at AdaCore is private (and with good reason). > > Whatever reasons might be, they aren't good. (:-() Oh no? What about top-secret Ada code from the military that triggers a bug in GNAT? >> If you use the FSF version of GNAT, you should use the corresponding >> bug database: Debian, Fedora or GCC upstream. > > Hmm, that would make sense only for bugs related to the compiler > environment, packaging etc. If the bug is a compiler problem, there is > no chance it can be fixed unless somebody is working on the compiler > itself. For example, there is a bug in assignment of controlled > objects. It crashes Debian, leaks in Fedora, fixed in GPL 2009. Should > it be reported? Where to? To those that you use actively. If you report it to Debian and I determine that the bug was not introduced by Debian, then I will forward it to the FSF. If you have a workaround, it is better to document it with the bug than let it remain unknown. The workaround may help other people avoid the bug and may also help people working on the compiler to fix the bug (if not already fixed). >> There are a few contributors external to AdaCore that provide bug >> fixes into the FSF GCC, sometimes ahead of AdaCore; I normally >> backport such fixes into the Debian version. Eventually, all bug >> fixes end up in both GNAT Pro/GPL and in FSF GCC. The keyword is >> "eventually"; the time lag can be months or years as you noted. > > So, when (if) GNAT GPL 2010 come, nothing will sufficiently change for > FSF? That is very disappointing. I hoped to jump off the GPL track > (not because of the license issue). FSF GCC 4.5.0 has just been released; this is roughly equivalent to GNAT GPL 2009. If you want the bleeding edge from the FSF, that's what you want. Unfortunately this is not packaged yet for Debian (and probably not for Fedora either, but I don't know). OTOH, if you can identify a patch in GCC 4.5.0 that fixes a bug (and does only that), then I'll be happy to backport it into Debian's GCC 4.4.4 for you. Browsing the changelog is, however, time-consuming. -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 21:26 ` Ludovic Brenta @ 2010-05-09 21:34 ` Yannick Duchêne (Hibou57) 2010-05-10 1:20 ` Ludovic Brenta 2010-05-10 9:41 ` Stephen Leake 0 siblings, 2 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-09 21:34 UTC (permalink / raw) Le Sun, 09 May 2010 23:26:10 +0200, Ludovic Brenta <ludovic@ludovic-brenta.org> a écrit: >> Whatever reasons might be, they aren't good. (:-() > > Oh no? What about top-secret Ada code from the military that triggers a > bug in GNAT? Yes, every one can understand that and probably did think about that while reading your words. However, a patch does not expose any private data, unless you claim some details all over the worlds. I'm pretty sure this is more a matter of GPL vs Pro than a matter of privacy (what privacy may be violated with a bug correction ?) -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 21:34 ` Yannick Duchêne (Hibou57) @ 2010-05-10 1:20 ` Ludovic Brenta 2010-05-10 1:26 ` Ludovic Brenta 2010-05-10 9:41 ` Stephen Leake 1 sibling, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-10 1:20 UTC (permalink / raw) Yannick Duchêne wrote on comp.lang.ada: > Le Sun, 09 May 2010 23:26:10 +0200, Ludovic Brenta > <ludovic@ludovic-brenta.org> a écrit: >>> Whatever reasons might be, they aren't good. (:-() >> >> Oh no? What about top-secret Ada code from the military that triggers a >> bug in GNAT? > Yes, every one can understand that and probably did think about that > while reading your words. However, a patch does not expose any private > data, unless you claim some details all over the worlds. The discussion was not about patches, it was about bug reports (which often contain reproducers that may be proprietary). The patches eventually make it into the FSF GCC; just look at the changelog. The only problem with this is that there is a delay between the time when the bugs are fixed in GNAT Pro (usually < 1 week after being reported) and the time they are fixed in FSF GCC (up to 2 years, sometimes even more). Not reporting a bug is the only certain way never to see it fixed. Therefore, if you don't have a support contract, report all your bugs. They will get fixed eventually. -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 1:20 ` Ludovic Brenta @ 2010-05-10 1:26 ` Ludovic Brenta 2010-05-25 20:40 ` Yannick Duchêne (Hibou57) 0 siblings, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-10 1:26 UTC (permalink / raw) I wrote on comp.lang.ada: > Not reporting a bug is the only certain way never to see it fixed. > Therefore, if you don't have a support contract, report all your bugs. > They will get fixed eventually. I might add this: If you do not report a bug, it will never be fixed. If you report a bug, one of several things can happen: - it is already fixed in GNAT Pro: then the fix will be in the next version of GCC and of GNAT GPL. In addition the bug that was hitherto private becomes public and a workaround may be found. - it it not already fixed in GNAT Pro: then it will be fixed in 2 years (usually less, though). A workaround may also be found in the mean time. Either way, nothing bad happens if you report a bug. PS. If you are jobless, you might try working on known compiler bugs and eventually join AdaCore :) -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 1:26 ` Ludovic Brenta @ 2010-05-25 20:40 ` Yannick Duchêne (Hibou57) 0 siblings, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-25 20:40 UTC (permalink / raw) Le Mon, 10 May 2010 03:26:56 +0200, Ludovic Brenta <ludovic@ludovic-brenta.org> a écrit: > PS. If you are jobless, you might try working on known compiler bugs and > eventually join AdaCore :) But you aren't an AdaCore member yourself, aren't you ? So, with due respect, how can I believe this supposition ? -- There is even better than a pragma Assert: a SPARK --# check. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 21:34 ` Yannick Duchêne (Hibou57) 2010-05-10 1:20 ` Ludovic Brenta @ 2010-05-10 9:41 ` Stephen Leake 2010-05-10 9:46 ` Ludovic Brenta 2010-05-10 18:47 ` Yannick Duchêne (Hibou57) 1 sibling, 2 replies; 95+ messages in thread From: Stephen Leake @ 2010-05-10 9:41 UTC (permalink / raw) "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes: > Le Sun, 09 May 2010 23:26:10 +0200, Ludovic Brenta > <ludovic@ludovic-brenta.org> a écrit: >>> Whatever reasons might be, they aren't good. (:-() >> >> Oh no? What about top-secret Ada code from the military that triggers a >> bug in GNAT? > Yes, every one can understand that and probably did think about that > while reading your words. However, a patch does not expose any private > data, unless you claim some details all over the worlds. > > I'm pretty sure this is more a matter of GPL vs Pro than a matter of > privacy (what privacy may be violated with a bug correction ?) The bug database includes the code that triggers the bug. It might be possible to expose only the fixes to public purview, but even the descriptions of the bug might contain some private information. It would take a lot of manual effort to present a "clean" public view. I'd rather AdaCore spend that effort on improving the tools. -- -- Stephe ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 9:41 ` Stephen Leake @ 2010-05-10 9:46 ` Ludovic Brenta 2010-05-10 14:29 ` sjw 2010-05-10 18:47 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-10 9:46 UTC (permalink / raw) Stephen Leake <stephen_leake@stephe-leake.org> writes: > "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes: > >> Le Sun, 09 May 2010 23:26:10 +0200, Ludovic Brenta >> <ludovic@ludovic-brenta.org> a écrit: >>>> Whatever reasons might be, they aren't good. (:-() >>> >>> Oh no? What about top-secret Ada code from the military that triggers a >>> bug in GNAT? >> Yes, every one can understand that and probably did think about that >> while reading your words. However, a patch does not expose any private >> data, unless you claim some details all over the worlds. >> >> I'm pretty sure this is more a matter of GPL vs Pro than a matter of >> privacy (what privacy may be violated with a bug correction ?) > > The bug database includes the code that triggers the bug. > > It might be possible to expose only the fixes to public purview, but > even the descriptions of the bug might contain some private information. > It would take a lot of manual effort to present a "clean" public view. > I'd rather AdaCore spend that effort on improving the tools. Actually, the fixes *are* exposed to public purview. This happens when AdaCore merge their fixes into GCC. Each patch appears as a self-contained email on the gcc-patches mailing list, complete with a technical description of the bug and even the AdaCore bug number; only, we don't know what triggered the bug, so it is difficult to relate the technical description to a publicly known bug trigger. -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 9:46 ` Ludovic Brenta @ 2010-05-10 14:29 ` sjw 2010-05-11 7:51 ` Ludovic Brenta 0 siblings, 1 reply; 95+ messages in thread From: sjw @ 2010-05-10 14:29 UTC (permalink / raw) On May 10, 10:46 am, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote: > Actually, the fixes *are* exposed to public purview. This happens when > AdaCore merge their fixes into GCC. Each patch appears as a > self-contained email on the gcc-patches mailing list, complete with a > technical description of the bug and even the AdaCore bug number; only, > we don't know what triggered the bug, so it is difficult to relate the > technical description to a publicly known bug trigger. I haven't seen any of these (I guess I joined that list between merges) but presumably the test suite does get updated (as with changes for other languages). ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 14:29 ` sjw @ 2010-05-11 7:51 ` Ludovic Brenta 2010-05-11 9:33 ` sjw 0 siblings, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-11 7:51 UTC (permalink / raw) Simon J. Wright wrote on comp.lang.ada: > On May 10, 10:46 am, Ludovic Brenta <ludo...@ludovic-brenta.org> > wrote: > >> Actually, the fixes *are* exposed to public purview. This happens when >> AdaCore merge their fixes into GCC. Each patch appears as a >> self-contained email on the gcc-patches mailing list, complete with a >> technical description of the bug and even the AdaCore bug number; only, >> we don't know what triggered the bug, so it is difficult to relate the >> technical description to a publicly known bug trigger. > > I haven't seen any of these (I guess I joined that list between > merges) but presumably the test suite does get updated (as with > changes for other languages). Here is a good, small example: http://gcc.gnu.org/ml/gcc-patches/2010-04/msg01528.html The patch includes a detailed description of the bug, i.e. the result of analyzing a bug report. The bug report itself (and any triggering code) is absent, as is the AdaCore bug number. The patch does contain a new test which triggers the bug; AdaCore constructed this from the analysis of the bug report. As you can see from the message, AdaCore applied this particular patch to both the mainline (i.e. the future GCC 4.6.0) and to the GCC 4.5 branch (i.e. the future GCC 4.5.1). GCC 4.6 entered Stage 1 on 2010-04-06 (immediately after the release of GCC 4.5.0) and the Ada patches started pouring in. The same happened for the Stage 1 of GCC 4.5.0 in March and April 2009; you can browse the mailing list archives and look for the tag "[Ada]" in the subject lines. PS. Thanks, Simon, for this: 2010-01-09 Simon Wright <simon@pushface.org> PR ada/42626 * gcc-interface/Makefile.in (gnatlib-shared-darwin): Add missing end-quote. -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 7:51 ` Ludovic Brenta @ 2010-05-11 9:33 ` sjw 0 siblings, 0 replies; 95+ messages in thread From: sjw @ 2010-05-11 9:33 UTC (permalink / raw) On May 11, 8:51 am, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote: > PS. Thanks, Simon, for this: > > 2010-01-09 Simon Wright <si...@pushface.org> > > PR ada/42626 > * gcc-interface/Makefile.in (gnatlib-shared-darwin): Add missing > end-quote. I have submitted a couple of others which were approved but not committed. I may not have found the right form of words to trigger a committer into action, and this all happened rather close to the 4.5.0 release, but in any case I'm having trouble getting the copyright assignment in place (low priority on the corporate radar, I guess), so I've held back on pinging the list ... ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 9:41 ` Stephen Leake 2010-05-10 9:46 ` Ludovic Brenta @ 2010-05-10 18:47 ` Yannick Duchêne (Hibou57) 1 sibling, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-10 18:47 UTC (permalink / raw) Le Mon, 10 May 2010 11:41:50 +0200, Stephen Leake <stephen_leake@stephe-leake.org> a écrit: > The bug database includes the code that triggers the bug. I didn't knew this was mandatory (now I know) -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 19:36 ` Dmitry A. Kazakov 2010-05-09 21:26 ` Ludovic Brenta @ 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) 2010-05-09 21:30 ` Yannick Duchêne (Hibou57) ` (3 more replies) 1 sibling, 4 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-09 21:28 UTC (permalink / raw) Le Sun, 09 May 2010 21:36:58 +0200, Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> a écrit: > Hmm, that would make sense only for bugs related to the compiler > environment, packaging etc. If the bug is a compiler problem, there is no > chance it can be fixed unless somebody is working on the compiler itself. > For example, there is a bug in assignment of controlled objects. It > crashes I was to report some bugs as well about GNAT (there was some about protected types, that's why your words make me though about it, however, there some others as well), and gave up to send bug reports when I've learned from people using the Pro version those bugs were already fixed for long. Yes, it seems obvious the differences between GNAT Pro and GNAT GPL are not only a matter of support (or lack of support) or of license (commercial application allowed vs disallowed) : it seems these are two different compilers. > So, when (if) GNAT GPL 2010 come, nothing will sufficiently change for > FSF? > That is very disappointing. I hoped to jump off the GPL track (not > because > of the license issue). That's why I like to hear Randy talking about its compiler and that's why I oftenly ask questions about this and that related to Ada compilers in the large. I would like to switch to another one... unfortunately, being jobless for too long, even something as cheap as Janus Ada Compiler is not accessible to me (and does not target BSD or UNIX-like too, that's another matter). I would not want to talk about things I'm not aware of, any way, what I am thinking about it (just personal beliefs) : obviously, an Ada compiler is lot of work, and anybody work better when receiving something in return which makes his/her life easier (what ever could say GPL advocates about it). I believe the GPL version is just far to be a priority for AdaCore (as long as I refer to some bugs I have talked about and for which I get an answer of the form “Hey, this is fixed for long in GNAT Pro”). AdaCore (or its ancestor) was initially mandated (is that the good word ?) to create a GPL Ada 95 compiler based on the GCC compiler chain (this was part of the requirements), to help ensure some good place for the Ada technology, to promote the language and its philosophy. This contract was largely fulfilled by AdaCore or its ancestor and its obligations about it has ended. AdaCore has no obligations at all concerning Ada 2005 nor any future Ada 2015 (or 2012... I don't know). Please, note the above are personal beliefs. P.S. What you are pointing about is not Fedora or UNIX-like specific, this is the same with the Windows version, this is mostly specific to the GPL version. P.P.S. I wonder why, being an owner of a GNAT Pro license, you need the GPL version ? You will get just less with the GPL version. -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) @ 2010-05-09 21:30 ` Yannick Duchêne (Hibou57) 2010-05-09 22:44 ` Simon Wright ` (2 subsequent siblings) 3 siblings, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-09 21:30 UTC (permalink / raw) > That's why I like to hear Randy talking about its compiler Sorry, I was to say “about *his* compiler” (shame on me... I'm not native English you know...) -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) 2010-05-09 21:30 ` Yannick Duchêne (Hibou57) @ 2010-05-09 22:44 ` Simon Wright 2010-05-10 7:54 ` Dmitry A. Kazakov 2010-05-10 8:02 ` Dmitry A. Kazakov 2010-05-10 14:15 ` GNAT Pro license (was: " Peter Hermann 3 siblings, 1 reply; 95+ messages in thread From: Simon Wright @ 2010-05-09 22:44 UTC (permalink / raw) "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes: > P.P.S. I wonder why, being an owner of a GNAT Pro license, you need > the GPL version ? You will get just less with the GPL version. I expect that very few private individuals have a GNAT Pro support contract! When developing open-source software, I wouldn't want to say to potential users such as yourself "my library works fine with GNAT Pro, too bad it doesn't work with GNAT GPL". ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 22:44 ` Simon Wright @ 2010-05-10 7:54 ` Dmitry A. Kazakov 0 siblings, 0 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-10 7:54 UTC (permalink / raw) On Sun, 09 May 2010 23:44:39 +0100, Simon Wright wrote: > "Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> writes: > >> P.P.S. I wonder why, being an owner of a GNAT Pro license, you need >> the GPL version ? You will get just less with the GPL version. > > I expect that very few private individuals have a GNAT Pro support > contract! Yes. As for me, I have GNAT Pro at work. The things I do privately I check against GNAT Pro. When I publish them I try to find a workaround in the GPL version. I do not report bugs from my private work to AdaCore, unless they also appear in the software our company develops. However there is a fair overlap, i.e. when AdaCore fixes one, that also fixes another. As I can judge GNAT Pro 6.3.x is pretty good by now. > When developing open-source software, I wouldn't want to say to > potential users such as yourself "my library works fine with GNAT Pro, > too bad it doesn't work with GNAT GPL". Exactly. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) 2010-05-09 21:30 ` Yannick Duchêne (Hibou57) 2010-05-09 22:44 ` Simon Wright @ 2010-05-10 8:02 ` Dmitry A. Kazakov 2010-05-10 18:45 ` Yannick Duchêne (Hibou57) 2010-05-10 14:15 ` GNAT Pro license (was: " Peter Hermann 3 siblings, 1 reply; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-10 8:02 UTC (permalink / raw) On Sun, 09 May 2010 23:28:26 +0200, Yannick Duch�ne (Hibou57) wrote: > I was to report some bugs as well about GNAT (there was some about > protected types, that's why your words make me though about it, however, > there some others as well), and gave up to send bug reports when I've > learned from people using the Pro version those bugs were already fixed > for long. > > Yes, it seems obvious the differences between GNAT Pro and GNAT GPL are > not only a matter of support (or lack of support) or of license > (commercial application allowed vs disallowed) : it seems these are two > different compilers. I don't think so. GPL looks like an outdated Pro. The real problem is that FSF is a "very outdated Pro," back to the times when GNAT was quite unstable (judging on the code I am writing). Maybe FSF will gain in 1-2 years, but then Ada 2012 will appear, breaking it again. Lack of a stable free compiler is a serious problem for Ada. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 8:02 ` Dmitry A. Kazakov @ 2010-05-10 18:45 ` Yannick Duchêne (Hibou57) 2010-05-10 21:00 ` Ludovic Brenta 2010-05-11 7:39 ` Dmitry A. Kazakov 0 siblings, 2 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-10 18:45 UTC (permalink / raw) Le Mon, 10 May 2010 10:02:45 +0200, Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> a écrit: > Maybe FSF will gain in 1-2 years, but then Ada 2012 will appear, breaking > it again. Yes, it happens I'm thinking about that trouble, as I'm waiting for long for the Programing By Contract (tm) capabilities (I use to be an Eiffel advocator for some times in the past). As I'm pretty sure they will not be support for that in the GCC or MinGW version, I was thinking I will probably go for a fall-back : just modify the actual version so that it will at least accept the syntax, so as to be able to write these pre- and post-conditions for documentation purpose. There will be not check at runtime (should be nice to ensure validity of expressions contained in the pre- and post- by the way), but this will at least allow to write it (a fall-back, as I said). 2012 in very close... -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 18:45 ` Yannick Duchêne (Hibou57) @ 2010-05-10 21:00 ` Ludovic Brenta 2010-05-10 22:17 ` Yannick Duchêne (Hibou57) 2010-05-11 7:39 ` Dmitry A. Kazakov 1 sibling, 1 reply; 95+ messages in thread From: Ludovic Brenta @ 2010-05-10 21:00 UTC (permalink / raw) Yannick Duchêne writes on comp.lang.ada: > Le Mon, 10 May 2010 10:02:45 +0200, Dmitry A. Kazakov > <mailbox@dmitry-kazakov.de> a écrit: >> Maybe FSF will gain in 1-2 years, but then Ada 2012 will appear, breaking >> it again. > Yes, it happens I'm thinking about that trouble, as I'm waiting for > long for the Programing By Contract (tm) capabilities (I use to be an > Eiffel advocator for some times in the past). As I'm pretty sure they > will not be support for that in the GCC or MinGW version, I was > thinking I will probably go for a fall-back : just modify the actual > version so that it will at least accept the syntax, so as to be able > to write these pre- and post-conditions for documentation > purpose. There will be not check at runtime (should be nice to ensure > validity of expressions contained in the pre- and post- by the way), > but this will at least allow to write it (a fall-back, as I said). > > 2012 in very close... So close, in fact, that the pre-, postconditions and invariants are already supported in GCC 4.4 (and therefore Debian) as implementation-defined pragmas: http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Precondition.html http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Postcondition.html http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Assert.html -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 21:00 ` Ludovic Brenta @ 2010-05-10 22:17 ` Yannick Duchêne (Hibou57) 2010-05-11 6:56 ` Ludovic Brenta 0 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-10 22:17 UTC (permalink / raw) Le Mon, 10 May 2010 23:00:32 +0200, Ludovic Brenta <ludovic@ludovic-brenta.org> a écrit: > So close, in fact, that the pre-, postconditions and invariants are > already supported in GCC 4.4 (and therefore Debian) as > implementation-defined pragmas: > > http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Precondition.html > http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Postcondition.html > http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Assert.html Lot of thanks for the news. So I have to guess MinGW (what I actually use) is a bit more outdated than GCC is. However, I will check if ever I missed a recent update. Nice point indeed -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 22:17 ` Yannick Duchêne (Hibou57) @ 2010-05-11 6:56 ` Ludovic Brenta 0 siblings, 0 replies; 95+ messages in thread From: Ludovic Brenta @ 2010-05-11 6:56 UTC (permalink / raw) Yannick Duchêne wrote on comp.lang.ada: > Le Mon, 10 May 2010 23:00:32 +0200, Ludovic Brenta > <ludo...@ludovic-brenta.org> a écrit:> So close, in fact, that the pre-, postconditions and invariants are > > already supported in GCC 4.4 (and therefore Debian) as > > implementation-defined pragmas: > > >http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Precondition.html > >http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Postcondition.... > >http://gcc.gnu.org/onlinedocs/gcc-4.4.4/gnat_rm/Pragma-Assert.html > > Lot of thanks for the news. So I have to guess MinGW (what I actually use) > is a bit more outdated than GCC is. However, I will check if ever I missed > a recent update. > > Nice point indeed BTW, GCC 4.4.0 was released on 2009-04-21 (and reached Debian unstable on 2009-07-26), so you've been waiting for 13 months for a feature that was already there... -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 18:45 ` Yannick Duchêne (Hibou57) 2010-05-10 21:00 ` Ludovic Brenta @ 2010-05-11 7:39 ` Dmitry A. Kazakov 2010-05-11 8:06 ` Yannick Duchêne (Hibou57) 2010-05-11 15:46 ` Pascal Obry 1 sibling, 2 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-11 7:39 UTC (permalink / raw) On Mon, 10 May 2010 20:45:18 +0200, Yannick Duch�ne (Hibou57) wrote: > Le Mon, 10 May 2010 10:02:45 +0200, Dmitry A. Kazakov > <mailbox@dmitry-kazakov.de> a �crit: >> Maybe FSF will gain in 1-2 years, but then Ada 2012 will appear, breaking >> it again. > Yes, it happens I'm thinking about that trouble, as I'm waiting for long > for the Programing By Contract (tm) capabilities (I use to be an Eiffel > advocator for some times in the past). I am not. Eiffel does it wrong. SPARK does it right. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 7:39 ` Dmitry A. Kazakov @ 2010-05-11 8:06 ` Yannick Duchêne (Hibou57) 2010-05-11 15:46 ` Pascal Obry 1 sibling, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 8:06 UTC (permalink / raw) Le Tue, 11 May 2010 09:39:34 +0200, Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> a écrit: >> Yes, it happens I'm thinking about that trouble, as I'm waiting for long >> for the Programing By Contract (tm) capabilities (I use to be an Eiffel >> advocator for some times in the past). > > I am not. Eiffel does it wrong. SPARK does it right. At that time, I did not ever knew there was such a thing as SPARK (which is still to be really learned to me... planed for very soon). At least, Eiffel was able to get a larger audience than SPARK, as there is a greater amount of peoples who know Eiffel than of peoples who know SPARK. So Eiffel still did something good in some way with its larger audience (if peoples who learned about Eiffel really goes further or not, did get benefit of what they discovered with it or not, or just used it as a fashion toy and did not learn anything of it, is an another story). -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 7:39 ` Dmitry A. Kazakov 2010-05-11 8:06 ` Yannick Duchêne (Hibou57) @ 2010-05-11 15:46 ` Pascal Obry 2010-05-11 16:05 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: Pascal Obry @ 2010-05-11 15:46 UTC (permalink / raw) 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. -- --|------------------------------------------------------ --| 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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 15:46 ` Pascal Obry @ 2010-05-11 16:05 ` Yannick Duchêne (Hibou57) 2010-05-11 16:09 ` Pascal Obry 2010-05-11 16:45 ` Dmitry A. Kazakov 0 siblings, 2 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 16:05 UTC (permalink / raw) Le Tue, 11 May 2010 17:46:58 +0200, Pascal Obry <pascal@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. While they can be compared in some way, there is indeed a big difference : Eiffel is runtime oriented, SPARK is static analysis oriented. -- pragma Asset ? Is that true ? Waaww... great ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:05 ` Yannick Duchêne (Hibou57) @ 2010-05-11 16:09 ` Pascal Obry 2010-05-11 16:09 ` Pascal Obry 2010-05-11 16:23 ` Yannick Duchêne (Hibou57) 2010-05-11 16:45 ` Dmitry A. Kazakov 1 sibling, 2 replies; 95+ messages in thread From: Pascal Obry @ 2010-05-11 16:09 UTC (permalink / raw) 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. -- --|------------------------------------------------------ --| 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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:09 ` Pascal Obry @ 2010-05-11 16:09 ` Pascal Obry 2010-05-11 17:08 ` stefan-lucks 2010-05-11 16:23 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: Pascal Obry @ 2010-05-11 16:09 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:09 ` Pascal Obry @ 2010-05-11 17:08 ` stefan-lucks 2010-05-11 16:39 ` Yannick Duchêne (Hibou57) 2010-05-11 17:35 ` Pascal Obry 0 siblings, 2 replies; 95+ messages in thread From: stefan-lucks @ 2010-05-11 17:08 UTC (permalink / raw) [-- Attachment #1: Type: TEXT/PLAIN, Size: 766 bytes --] 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! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 17:08 ` stefan-lucks @ 2010-05-11 16:39 ` Yannick Duchêne (Hibou57) 2010-05-11 19:45 ` Yannick Duchêne (Hibou57) 2010-05-11 17:35 ` Pascal Obry 1 sibling, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 16:39 UTC (permalink / raw) Le Tue, 11 May 2010 19:08:16 +0200, <stefan-lucks@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:39 ` Yannick Duchêne (Hibou57) @ 2010-05-11 19:45 ` Yannick Duchêne (Hibou57) 2010-05-11 23:44 ` Yannick Duchêne (Hibou57) 0 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 19:45 UTC (permalink / raw) Le Tue, 11 May 2010 18:39:52 +0200, Yannick Duchêne (Hibou57) <yannick_duchene@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 19:45 ` Yannick Duchêne (Hibou57) @ 2010-05-11 23:44 ` Yannick Duchêne (Hibou57) 2010-05-12 12:12 ` Mark Lorenzen 0 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 23:44 UTC (permalink / raw) Le Tue, 11 May 2010 21:45:45 +0200, Yannick Duchêne (Hibou57) <yannick_duchene@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 23:44 ` Yannick Duchêne (Hibou57) @ 2010-05-12 12:12 ` Mark Lorenzen 2010-05-12 14:55 ` Yannick Duchêne (Hibou57) 0 siblings, 1 reply; 95+ messages in thread From: Mark Lorenzen @ 2010-05-12 12:12 UTC (permalink / raw) On 12 Maj, 01:44, Yannick Duchêne (Hibou57) <yannick_duch...@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 12:12 ` Mark Lorenzen @ 2010-05-12 14:55 ` Yannick Duchêne (Hibou57) 0 siblings, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-12 14:55 UTC (permalink / raw) Le Wed, 12 May 2010 14:12:31 +0200, Mark Lorenzen <mark.lorenzen@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 17:08 ` stefan-lucks 2010-05-11 16:39 ` Yannick Duchêne (Hibou57) @ 2010-05-11 17:35 ` Pascal Obry 2010-05-11 18:06 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: Pascal Obry @ 2010-05-11 17:35 UTC (permalink / raw) Le 11/05/2010 19:08, stefan-lucks@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 17:35 ` Pascal Obry @ 2010-05-11 18:06 ` Yannick Duchêne (Hibou57) 0 siblings, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 18:06 UTC (permalink / raw) Le Tue, 11 May 2010 19:35:43 +0200, Pascal Obry <pascal@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:09 ` Pascal Obry 2010-05-11 16:09 ` Pascal Obry @ 2010-05-11 16:23 ` Yannick Duchêne (Hibou57) 2010-05-11 16:41 ` J-P. Rosen 1 sibling, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 16:23 UTC (permalink / raw) Le Tue, 11 May 2010 18:09:14 +0200, Pascal Obry <pascal@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:23 ` Yannick Duchêne (Hibou57) @ 2010-05-11 16:41 ` J-P. Rosen 0 siblings, 0 replies; 95+ messages in thread From: J-P. Rosen @ 2010-05-11 16:41 UTC (permalink / raw) Yannick Duchï¿œne (Hibou57) a ï¿œcrit : > Le Tue, 11 May 2010 18:09:14 +0200, Pascal Obry <pascal@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@adalog.fr) Visit Adalog's web site at http://www.adalog.fr ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:05 ` Yannick Duchêne (Hibou57) 2010-05-11 16:09 ` Pascal Obry @ 2010-05-11 16:45 ` Dmitry A. Kazakov 2010-05-11 19:21 ` Yannick Duchêne (Hibou57) 2010-05-12 8:41 ` stefan-lucks 1 sibling, 2 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-11 16:45 UTC (permalink / raw) 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@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:45 ` Dmitry A. Kazakov @ 2010-05-11 19:21 ` Yannick Duchêne (Hibou57) 2010-05-12 8:41 ` stefan-lucks 1 sibling, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-11 19:21 UTC (permalink / raw) Le Tue, 11 May 2010 18:45:14 +0200, Dmitry A. Kazakov <mailbox@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-11 16:45 ` Dmitry A. Kazakov 2010-05-11 19:21 ` Yannick Duchêne (Hibou57) @ 2010-05-12 8:41 ` stefan-lucks 2010-05-12 14:52 ` Yannick Duchêne (Hibou57) ` (2 more replies) 1 sibling, 3 replies; 95+ messages in thread From: stefan-lucks @ 2010-05-12 8:41 UTC (permalink / raw) [-- Attachment #1: Type: TEXT/PLAIN, Size: 2441 bytes --] 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! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 8:41 ` stefan-lucks @ 2010-05-12 14:52 ` Yannick Duchêne (Hibou57) 2010-05-12 15:59 ` Phil Thornley 2010-05-12 15:37 ` Dmitry A. Kazakov 2010-05-13 0:33 ` Yannick Duchêne (Hibou57) 2 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-12 14:52 UTC (permalink / raw) Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 14:52 ` Yannick Duchêne (Hibou57) @ 2010-05-12 15:59 ` Phil Thornley 2010-05-12 16:49 ` Yannick Duchêne (Hibou57) 0 siblings, 1 reply; 95+ messages in thread From: Phil Thornley @ 2010-05-12 15:59 UTC (permalink / raw) On 12 May, 15:52, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr> wrote: [snip] > > 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). > Sorry, Yannick, but you are wrong. Recursion between subprograms in different packages is prohibited by the rule that mutual inheritance between packages is not allowed. Recursion between subprograms in a single package (including self- recursion) is prohibited by the rule that a subprogram cannot be called until all of its body has been declared. I don't think this is mentioned in the SPARK language description, but if you violate this rule you get semantic error 163: "Semantic Error :163: Subprogram XXX cannot be called from here. SPARK contains rules to prevent construction of programs containing recursive subprogram calls; this error message occurs if a procedure or function is called before its body has been declared. Re-ordering of subprogram bodies in the package concerned will be required." I haven't seen the latest SPARK version yet (still waiting for the GPL version) but I would be very surprised if this has changed since the last version. Cheers, Phil ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 15:59 ` Phil Thornley @ 2010-05-12 16:49 ` Yannick Duchêne (Hibou57) 2010-05-13 8:05 ` Phil Thornley 0 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-12 16:49 UTC (permalink / raw) Le Wed, 12 May 2010 17:59:21 +0200, Phil Thornley <phil.jpthornley@googlemail.com> a écrit: > Sorry, Yannick, but you are wrong. > > Recursion between subprograms in different packages is prohibited by > the rule that mutual inheritance between packages is not allowed. That's one of that severe limitations so (noted, as I'm learning). > Recursion between subprograms in a single package (including self- > recursion) is prohibited by the rule that a subprogram cannot be > called until all of its body has been declared. I don't think this is > mentioned in the SPARK language description, but if you violate this > rule you get semantic error 163: An attempt to give an answer : I had to drop recursivity in a JavaScript application, because this was a long process and JavaScript has no support at all for multi-tasking (except with some tricks relying on pop-up windows... which unfortunately browsers blocks). So I had to rely on timer, bounded execution chunk (kind of cooperative multitasking as it was with Windows 3.1) and had to re-implement recursivity on top of an array used as a stack. The “process” was reloading its previous state from variables each time it was resuming, and as there was obviously no way to restore the stack pointer (JavaScript is not C or assembly you know), I had to re-implement the stack this way. I suppose this kind of recursivity would be OK. May be this help analysis after all ? And there are recursivities which can be dropped, like the one of binary-search (a kind of final recursivity, and that is a common optimization in functional languages to drop these) > I haven't seen the latest SPARK version yet (still waiting for the GPL > version) but I would be very surprised if this has changed since the > last version. > > Cheers, > > Phil The one I've installed yesterday is version 8.1.1. Not version 9 Mark L talked about, however, this one seems to already have support for generics. -- pragma Asset ? Is that true ? Waaww... great ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 16:49 ` Yannick Duchêne (Hibou57) @ 2010-05-13 8:05 ` Phil Thornley 0 siblings, 0 replies; 95+ messages in thread From: Phil Thornley @ 2010-05-13 8:05 UTC (permalink / raw) On 12 May, 17:49, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr> wrote: > ... The “process” was reloading its previous state from > variables each time it was resuming, and as there was obviously no way to > restore the stack pointer (JavaScript is not C or assembly you know), I > had to re-implement the stack this way. > > I suppose this kind of recursivity would be OK. Sure - you can make the data structures as complicated as you like - the recursion rules in SPARK only apply to the code structures. Cheers, Phil ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 8:41 ` stefan-lucks 2010-05-12 14:52 ` Yannick Duchêne (Hibou57) @ 2010-05-12 15:37 ` Dmitry A. Kazakov 2010-05-12 16:06 ` Yannick Duchêne (Hibou57) 2010-05-12 18:10 ` stefan-lucks 2010-05-13 0:33 ` Yannick Duchêne (Hibou57) 2 siblings, 2 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-12 15:37 UTC (permalink / raw) On Wed, 12 May 2010 10:41:03 +0200, stefan-lucks@see-the.signature wrote: > 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 ... 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 respect. The point is that run-time checks contribute nothing to correctness either partial or not. Because a partially incorrect program remains partially incorrect independently on whether you check that or not: SPARK makes *some* incorrect programs invalid. Eiffel does not. That is the difference. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 15:37 ` Dmitry A. Kazakov @ 2010-05-12 16:06 ` Yannick Duchêne (Hibou57) 2010-05-12 17:24 ` Dmitry A. Kazakov 2010-05-12 18:10 ` stefan-lucks 1 sibling, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-12 16:06 UTC (permalink / raw) Le Wed, 12 May 2010 17:37:44 +0200, Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> a écrit: > 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 respect. 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 way, 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 better 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 discover what's wrong. Obviously, static checker does not even need input which are 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. Detecting 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 to face an error like “this class invariant was violated” than “this access to this memory address failed”. 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 is 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 “C, assembly and Eiffel are all the same and none provided better proof an application may at least run partially good” is a lot said (it is by the way as much true that jocks and teasing kept apart, C is not the same as assembly) And like Pascal said : “Eiffel is far more easier than SPARK” (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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 16:06 ` Yannick Duchêne (Hibou57) @ 2010-05-12 17:24 ` Dmitry A. Kazakov 2010-05-12 18:09 ` Georg Bauhaus ` (2 more replies) 0 siblings, 3 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-12 17:24 UTC (permalink / raw) On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: > 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 better > to catch error the sooner and understand why this was an error. 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. > About expression now, although understandability of a source does not > provide proof, this help to at least make partial assertions and discover > what's wrong. No more than an appropriately placed if-statement, tracing call, debugging break point etc. > It is best to > face an error like “this class invariant was violated” than “this access > to this memory address failed”. The text used in error message is up to the programmer. My objection is not that what Eiffel offers is useless. The objection is that it has nothing to do with contracts (in its normal meaning) or with design by. These are no more than *debugging* tools. Using the terms pre-, postcondition, invariant is also misleading. > And like Pascal said : “Eiffel is far more easier than SPARK” (you cannot > request every one to know SPARK, and you help them when you provide them > something like Eiffel). Yes, but you do not want to prove everything, which is impossible anyway. What Ada lacks is better contracts specified by the programmer only when he wishes to. E,g, exception contracts, statements about purity of a function, upper bound of stack use etc. IMO, Ada does not need Eiffel-like pre- postconditions, assertions etc. They add nothing to safety and thus to Ada. It would be enough to introduce raise when <condition>; and close the theme. (Yes I heard the argument that one can use them in declarations. I don't think that is a good idea. I don't like exceptions from declarations.) Ada had dynamic constraints long before Eiffel. If one wished to extend this feature, it is welcome. Just do not call it "error check", when you use the subtype Positive. Tie it to subtypes. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 17:24 ` Dmitry A. Kazakov @ 2010-05-12 18:09 ` Georg Bauhaus 2010-05-12 18:33 ` Dmitry A. Kazakov 2010-05-15 0:17 ` Robert A Duff 2010-05-12 18:15 ` Georg Bauhaus 2010-05-25 20:45 ` Yannick Duchêne (Hibou57) 2 siblings, 2 replies; 95+ messages in thread From: Georg Bauhaus @ 2010-05-12 18:09 UTC (permalink / raw) On 12.05.10 19:24, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: > >> 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 better >> to catch error the sooner and understand why this was an error. > > Yes, it is better but that is not the point. Being better is precisely the point (of DbC). DbC talks about proof obligations, not about provability. > there is no > substantial difference between Eiffel precondition and C's if statement > beyond syntax sugar, and that if-statement is less misleading. "If" is - much more flexible and - totally unspecific and - not integrated with, e.g. rescue clauses; - needs bodies You can emulate anything with "if" or write assembler, though ... . >> About expression now, although understandability of a source does not >> provide proof, this help to at least make partial assertions and discover >> what's wrong. > > No more than an appropriately placed if-statement, tracing call, debugging > break point etc. You cannot place an "if" in a specification. If you say Precondition: Has-Such-And-Such; then this is effectively raise when not Has-Such-And-Such; Except that smart tools do not need to understand the full program including its bodies in order to infer a precondition. >> It is best to >> face an error like “this class invariant was violated” than “this access >> to this memory address failed”. > > The text used in error message is up to the programmer. My objection is not > that what Eiffel offers is useless. The objection is that it has nothing to > do with contracts (in its normal meaning) or with design by. These are no > more than *debugging* tools. Using the terms pre-, postcondition, invariant > is also misleading. What is "breach of contract" in your world? Anything that is not yielding a full proof of everything is a debugging tool. So what? Should we therefore bend the normal, worldly definition of "contract" to mean something that can never be had? > What Ada lacks is better contracts specified by the programmer only when he > wishes to. E,g, exception contracts, statements about purity of a function, > upper bound of stack use etc. Raising of exceptions is an integral part of DbC specs. Purity: postcondition: interesting_1 = interesting_1'old and interesting_2 = interesting_2'old and ...; Stack usage: precondition: avail = max_avail - 140; > Ada had dynamic constraints long before Eiffel. If one wished to extend > this feature, it is welcome. Just do not call it "error check", when you > use the subtype Positive. Tie it to subtypes. How would you specify subtype Even is ...; ? ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 18:09 ` Georg Bauhaus @ 2010-05-12 18:33 ` Dmitry A. Kazakov 2010-05-12 18:53 ` Georg Bauhaus 2010-05-15 0:17 ` Robert A Duff 1 sibling, 1 reply; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-12 18:33 UTC (permalink / raw) On Wed, 12 May 2010 20:09:49 +0200, Georg Bauhaus wrote: > On 12.05.10 19:24, Dmitry A. Kazakov wrote: >> On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: >> >>> 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 better >>> to catch error the sooner and understand why this was an error. >> >> Yes, it is better but that is not the point. > > Being better is precisely the point (of DbC). > DbC talks about proof obligations, not about provability. Who is obliged to whom in what? >> there is no >> substantial difference between Eiffel precondition and C's if statement >> beyond syntax sugar, and that if-statement is less misleading. > > "If" is > - much more flexible and > - totally unspecific and > - not integrated with, e.g. rescue clauses; > - needs bodies > > You can emulate anything with "if" or write assembler, though ... . Yes, but all above is not substantial. >>> About expression now, although understandability of a source does not >>> provide proof, this help to at least make partial assertions and discover >>> what's wrong. >> >> No more than an appropriately placed if-statement, tracing call, debugging >> break point etc. > > You cannot place an "if" in a specification. The answer was in my post. You have skipped out. OK, it was that exceptions from declarations is not a good idea. And considering it more deeply, Eiffel cannot do it either, because specifications are static things. What you meant is actually "if" in declarations elaboration, which is quite possible. >>> It is best to >>> face an error like “this class invariant was violated” than “this access >>> to this memory address failed”. >> >> The text used in error message is up to the programmer. My objection is not >> that what Eiffel offers is useless. The objection is that it has nothing to >> do with contracts (in its normal meaning) or with design by. These are no >> more than *debugging* tools. Using the terms pre-, postcondition, invariant >> is also misleading. > > What is "breach of contract" in your world? A case for the court. >> What Ada lacks is better contracts specified by the programmer only when he >> wishes to. E,g, exception contracts, statements about purity of a function, >> upper bound of stack use etc. > > Raising of exceptions is an integral part of DbC specs. And buffer overflow is an integral part of C... I meant static contracts, statically checked, if that was not clear. It don't need a shortcut for if-then-raise. >> Ada had dynamic constraints long before Eiffel. If one wished to extend >> this feature, it is welcome. Just do not call it "error check", when you >> use the subtype Positive. Tie it to subtypes. > > How would you specify > > subtype Even is ...; ? Ada's syntax is: subtype <name> is <name> <constraint>; -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 18:33 ` Dmitry A. Kazakov @ 2010-05-12 18:53 ` Georg Bauhaus 2010-05-12 21:57 ` Dmitry A. Kazakov 0 siblings, 1 reply; 95+ messages in thread From: Georg Bauhaus @ 2010-05-12 18:53 UTC (permalink / raw) On 12.05.10 20:33, Dmitry A. Kazakov wrote: >> Being better is precisely the point (of DbC). >> DbC talks about proof obligations, not about provability. > > Who is obliged to whom in what? By being a programmer subscribing to the principles of DbC, you are obliged to show that the components of your system obey the components' contracts. The compiler and run-time try to help you achieving this goal. >>>> About expression now, although understandability of a source does not >>>> provide proof, this help to at least make partial assertions and discover >>>> what's wrong. >>> >>> No more than an appropriately placed if-statement, tracing call, debugging >>> break point etc. >> >> You cannot place an "if" in a specification. > > The answer was in my post. You have skipped out. OK, it was that exceptions > from declarations is not a good idea. And considering it more deeply, > Eiffel cannot do it either, because specifications are static things. Which set of "specifications" has only static things in it? Why exclude conditionals whose results cannot reasonably be computed by the compiler but (a) can be computed for every single case occuring in the executing program (b) can guide the author of a client of a DbC component? For example, assume that Is_Prime(N) is a precondition of sub P. Furthermore, TIME(Is_Prime(N)) >> PERMISSIBLE_TIME. Then, still, PRE: Is_Prime (N) expresses an obligation, part of a contract: Don't call P unless N is prime, no matter whether or not assertion checking is in effect. (A DbC principle is that assertions are *not* a replacement for checking input (at the client side).) >> What is "breach of contract" in your world? > > A case for the court. What's the court (speaking of programs)? >>> What Ada lacks is better contracts specified by the programmer only when he >>> wishes to. E,g, exception contracts, statements about purity of a function, >>> upper bound of stack use etc. >> >> Raising of exceptions is an integral part of DbC specs. > > And buffer overflow is an integral part of C... I meant static contracts, > statically checked, if that was not clear. It wasn't clear to me that you wanted a mathematically closed structure to be the only legitimate substance of "contract". I'm a programmer. If I "design" anything, it is a program whose parts need to interact in a way that meets some almost entirely non-mathematical specification. I try to add some formality to the whole thing. This helps. I wish I had static type checking for a start! >> How would you specify >> >> subtype Even is ...; ? > > Ada's syntax is: > > subtype <name> is <name> <constraint>; What will static <name> and static <constraint> be for subtype Even? ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 18:53 ` Georg Bauhaus @ 2010-05-12 21:57 ` Dmitry A. Kazakov 2010-05-13 2:03 ` Georg Bauhaus 0 siblings, 1 reply; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-12 21:57 UTC (permalink / raw) On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote: > On 12.05.10 20:33, Dmitry A. Kazakov wrote: > >>> Being better is precisely the point (of DbC). >>> DbC talks about proof obligations, not about provability. >> >> Who is obliged to whom in what? > > By being a programmer subscribing to the principles of DbC, > you are obliged to show that the components of your system > obey the components' contracts. The compiler and run-time > try to help you achieving this goal. A C programmer would tell you same story about merits of pointers, casts and preprocessor. >>> You cannot place an "if" in a specification. >> >> The answer was in my post. You have skipped out. OK, it was that exceptions >> from declarations is not a good idea. And considering it more deeply, >> Eiffel cannot do it either, because specifications are static things. > > Which set of "specifications" has only static things in it? > Why exclude conditionals whose results cannot reasonably > be computed by the compiler but > > (a) can be computed for every single case occuring in the > executing program If they can for *every* case, they are statically checkable, per definition. > (b) can guide the author of a client of a DbC component? I don't know what does it mean technically. Doesn't core dump guide programmers? Blue screens certainly do. > For example, assume that Is_Prime(N) is a precondition of sub P. > Furthermore, TIME(Is_Prime(N)) >> PERMISSIBLE_TIME. > Then, still, PRE: Is_Prime (N) expresses an obligation, > part of a contract: Don't call P unless N is prime, > no matter whether or not assertion checking is in effect. char X [80]; // Don't use X[80], X[81], no matter etc. > (A DbC principle is that assertions are *not* a replacement > for checking input (at the client side).) Exactly. Assertion is not a check. You said this. >>> What is "breach of contract" in your world? >> >> A case for the court. > > What's the court (speaking of programs)? A code revision. > I'm a programmer. If I "design" anything, it is a program whose > parts need to interact in a way that meets some almost entirely > non-mathematical specification. Mathematics has nothing to do with this. It is about a clear distinction between a contract and a condition, how undesirable it could be but nevertheless it is a condition, which you, as a programmer are obliged to consider as *possible*. Eiffel gives you an illusion of safety. This is even worse than C, which openly declares "I am dangerous." Simply consider the following rule: my program shall handle each exception I introduce. Objections? Then consider exceptions from assertions. >>> How would you specify >>> >>> subtype Even is ...; ? >> >> Ada's syntax is: >> >> subtype <name> is <name> <constraint>; > > What will static <name> and static <constraint> be for subtype Even? No, in Ada <constraint> is not required to be static. Example: procedure F (A : String) is subtype Span is Integer range A'Range; -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 21:57 ` Dmitry A. Kazakov @ 2010-05-13 2:03 ` Georg Bauhaus 2010-05-13 8:39 ` Dmitry A. Kazakov 0 siblings, 1 reply; 95+ messages in thread From: Georg Bauhaus @ 2010-05-13 2:03 UTC (permalink / raw) On 5/12/10 11:57 PM, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote: > >> On 12.05.10 20:33, Dmitry A. Kazakov wrote: >> >>>> Being better is precisely the point (of DbC). >>>> DbC talks about proof obligations, not about provability. >>> >>> Who is obliged to whom in what? >> >> By being a programmer subscribing to the principles of DbC, >> you are obliged to show that the components of your system >> obey the components' contracts. The compiler and run-time >> try to help you achieving this goal. > > A C programmer would tell you same story about merits of pointers, casts > and preprocessor. All of these features of C have merits besides what else they may have. But they sure don't warrant dismissing DbC? A C programmer is "right" when he tells an *analogous* story that competent C programmers will avoid typical mistakes by correct use of C features. ... whenever a competent C programmer is defined to be one who avoids these mistakes... A C programmer's tool set is difficult to use for correct, portable programs. For example, ADTs are mostly emulated via style and conventions, by programmers working correctly; there is little direct language support for ADTs in C. Ada seems better here. But before the arrival of preconditions etc. Ada didn't have that much to offer to programmers wanting to state sets of permissible values, for example for subprogram parameters. Or wanting to state relations required to hold between parameters. Ada subtypes, e.g. scalars, are poorly equipped for this style of value set specification, AFAICS. They do establish two implicit preconditions (>= S'First and <= S'Last). And these little things seem to do miracles already, judging by the model train study of McCormick. A Qi style type system could do more via types but is not to be in Ada any time soon, is it? Let alone a statically verifiable one. Hence my insistence on a worked out example of a subtype Even with a static specification of the intended value set, one that can be written by a single programmer. Alternatively, as is, package P is type Number is range 1 .. 10; function Compute (A, B: Number) return Number with Precondition => A >= B; type Number_Too is range 0 .. 10_000_000; function Compute_Too (A, B: Number_Too) return Number_Too with Precondition (A + B = 5_000_000); -- etc., with Precondition's predicate in O(P(N)); end; (Such specifications, if they were to be being static, would exclude a test of A in relation to B at run time, for example to reverse their order in a recursive call as needed. It would also exclude a simple test at run time that A + B = 5_000_000.) A distinguishing property of DbC visible here is that a programmer will *see* the contract (or part thereof). Whatever implementation of Compute will later be provided, he does not need to infer arguments in proper calls of Compute from looking at the code of the body (or its object code). Surely code review can provide results insofar as there will be no doubt about what (current!) preconditions can be inferred from the code. The code of the current implementation! Code review, meant as an alternative to giving preconditions, just seems impractical in the general case. Unlike DbC. >> Which set of "specifications" has only static things in it? >> Why exclude conditionals whose results cannot reasonably >> be computed by the compiler but >> >> (a) can be computed for every single case occuring in the >> executing program > > If they can for *every* case, they are statically checkable, per > definition. "Every case" cannot "reasonably be computed by the compiler". Continuing the examples above. (This argument is also somewhere in OOSC2.) >> (b) can guide the author of a client of a DbC component? > > I don't know what does it mean technically. Contractually, it means "do as the preconditions say." And the preconditions say more than an Ada type can ever say! A subprogram is perfect if there is little else to say than "of this subtype", but that isn't always possible. A responsible programmer will then write calls ensuring that an argument is even. Or that the first argument is greater than the second. The client programmer can arrange for these conditions only because he has clear, formal instructions written as preconditions. The contract guides him, it tells what to do. Why not have a computer language help us express these preconditions? Some can even be checked when we develop our software. A paradoxical consequence of this style of invitation (to please write your client code properly) is this: "Under no circumstances shall the body of a routine ever test for the routine's precondition." -- OOCS2, p.343 IOW, no redundant checks. Note that this is true with assertion checking on or off. And yes, the author does say something about defensive programming at the microscopic (routine) level: it should be avoided in DbC systems in favor of correct software. Have DbC help you write correct software instead. (There is more to say here, e.g. about the "magic" that is needed to program a correct defence...) >> For example, assume that Is_Prime(N) is a precondition of sub P. >> Furthermore, TIME(Is_Prime(N))>> PERMISSIBLE_TIME. >> Then, still, PRE: Is_Prime (N) expresses an obligation, >> part of a contract: Don't call P unless N is prime, >> no matter whether or not assertion checking is in effect. > > char X [80]; // Don't use X[80], X[81], no matter etc. Yes, and don't use X[-200]. But you can. OTOH: function Access_Element (S: String_80; X: Index_80); function Careful (S: String_80; X: Index_80) with Precondition => X rem 2 = 1; How would you write a statically checked version? >> (A DbC principle is that assertions are *not* a replacement >> for checking input (at the client side).) > > Exactly. Assertion is not a check. You said this. What check means, exactly, is important. DbC assertion checking or monitoring can turn assertions into run-time checks; these checks turned can be on or off, like pragma Assert in Ada. Input checking is something completely different. Input to a routine comes from a programmer's call. It is the programmer's obligation to make sure input is valid. It is not the called routine's obligation. Another input is I/O, which by the rules is checked for validity, too. >>>> What is "breach of contract" in your world? >>> >>> A case for the court. >> >> What's the court (speaking of programs)? > > A code revision. How do you become aware of a broken contract? Statically? Dynamically? Typically, I think, you notice a malfunctioning program or an exception occurrence; same with DbC. But DbC is also about specifying what you want before you have an issue and before you have a result of code review. In this sense, DbC extends an Ada spec. I guess you can even use DbC assertions in code review comparing results with your contracts. >> I'm a programmer. If I "design" anything, it is a program whose >> parts need to interact in a way that meets some almost entirely >> non-mathematical specification. > > Mathematics has nothing to do with this. It is about a clear distinction > between a contract and a condition, how undesirable it could be but > nevertheless it is a condition, which you, as a programmer are obliged to > consider as *possible*. Eiffel gives you an illusion of safety. No. Eiffel marketing claims that a fully proven DbC program is 100% bug free. I can't imagine that compiler makers will claim that such a program is guaranteed to automatically produce correct results for each input and presume that every input can be successfully tested for validity. They know about SPARK and TTBOMK they won't claim DbC to effect more than SPARK does. > Simply consider > the following rule: my program shall handle each exception I introduce. > Objections? No objection. > Then consider exceptions from assertions. That is what Eiffel's rescue mechanism is about. Failed assertions are one exception case (defined in $12.1 of OOSC2). BTW, there is a rule in DbC about the correctness of exception handlers of primitive operations. The rule starts from a call of a primitive operation that fails (to terminate its execution in a state satisfying the primitive operation's contract {post(x) and INV}. The primitive operation's exception handler is correct if it establishes its type's INV before propagating the exception to its caller. I am mentioning this to draw attention to the fact that DbC is not just a thin, fluffy wrapper for "raise when" or pragma Assert. If it were the latter, then it would be a bit like C style roll-your-own. >>>> How would you specify >>>> >>>> subtype Even is ...; ? >>> >>> Ada's syntax is: >>> >>> subtype<name> is<name> <constraint>; >> >> What will static<name> and static<constraint> be for subtype Even? > > No, in Ada<constraint> is not required to be static. Example: > > procedure F (A : String) is > subtype Span is Integer range A'Range; > Is the constraint, not to be static, then part of the contractual specification of subtype Even? ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-13 2:03 ` Georg Bauhaus @ 2010-05-13 8:39 ` Dmitry A. Kazakov 2010-05-14 23:45 ` Georg Bauhaus 0 siblings, 1 reply; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-13 8:39 UTC (permalink / raw) On Thu, 13 May 2010 04:03:38 +0200, Georg Bauhaus wrote: > All of these features of C have merits besides what else > they may have. But they sure don't warrant dismissing DbC? No. The point was about lack of substance in DbC as promoted by Eiffel. > Ada seems better here. But before the arrival of preconditions > etc. Ada didn't have that much to offer to programmers wanting > to state sets of permissible values, for example for subprogram > parameters. Ada has strong types. "A set of permissible values" does not look like that. > Ada subtypes, e.g. scalars, are poorly equipped for this style of > value set specification, AFAICS. They do establish two implicit > preconditions (>= S'First and <= S'Last). These are not preconditions, but invariants. > A Qi style type system could do more via types but is not to be in Ada > any time soon, is it? I don't know. If Ada designers will keep on driving Ada into a dynamically typed language, then probably never. > package P is > > type Number is range 1 .. 10; > function Compute (A, B: Number) return Number > with Precondition => A >= B; I don't understand this notation. > (Such specifications, if they were to be being static, would exclude > a test of A in relation to B at run time, You need not to specify anything you cannot check... As somebody said, do not check for bugs you aren't going to fix. (:-)) > A distinguishing property of DbC visible here is > that a programmer will *see* the contract (or part thereof). I do not accept "preconditions" in the operations, which are not statically true: function "/" (X, Y : Number) return Number -- Wrong! pre : Y /= 0.0; function "/" (X, Y : Number) return Number -- Right! post : result = X/Y or else Constraint_Error; >>> Which set of "specifications" has only static things in it? >>> Why exclude conditionals whose results cannot reasonably >>> be computed by the compiler but >>> >>> (a) can be computed for every single case occuring in the >>> executing program >> >> If they can for *every* case, they are statically checkable, per >> definition. > > "Every case" cannot "reasonably be computed by the compiler". Either they can or cannot. You said they can, but then added "unreasonably can", or "reasonably cannot", whatever. Sound like Eiffel's contracts, x is even, not really even, we wanted it be even... (:-)) >>> (b) can guide the author of a client of a DbC component? >> >> I don't know what does it mean technically. > > Contractually, it means "do as the preconditions say." Like "do as comments say"? Note, since your "preconditions" are not static, how can you know *what* they say, in order to do as they do? Eiffel masters with easily. Its DbC is "do as you want, we'll see later." But I think that the honor of inventing this design principle by right belongs to C... > "Under no circumstances shall the body of a routine ever > test for the routine's precondition." -- OOCS2, p.343 > > IOW, no redundant checks. No, it would be *inconsistent* checks. No program can check itself. Eiffel pre- and postconditions fall into this category. Of course, I can imagine a compiler which would use a separate CPU core to check pre- and ponstconditions at tun-time. but that is beyond the point. >>> For example, assume that Is_Prime(N) is a precondition of sub P. >>> Furthermore, TIME(Is_Prime(N))>> PERMISSIBLE_TIME. >>> Then, still, PRE: Is_Prime (N) expresses an obligation, >>> part of a contract: Don't call P unless N is prime, >>> no matter whether or not assertion checking is in effect. >> >> char X [80]; // Don't use X[80], X[81], no matter etc. > > Yes, and don't use X[-200]. But you can. OTOH: > > function Access_Element (S: String_80; X: Index_80); > > function Careful (S: String_80; X: Index_80) > with Precondition => X rem 2 = 1; > > How would you write a statically checked version? Trivially: function Careful (S: String_80; X: Index_80) with Precondition True; with Postcondition <whatever> or Constraint_Error >>> (A DbC principle is that assertions are *not* a replacement >>> for checking input (at the client side).) >> >> Exactly. Assertion is not a check. You said this. > > What check means, exactly, is important. Error_Check (P) => P is incorrect other things you mentioned are control flow control statements. It is really simply: an error/correctness check is a statement about the program behavior. If-statement/exception etc is the program behavior. >>>>> What is "breach of contract" in your world? >>>> >>>> A case for the court. >>> >>> What's the court (speaking of programs)? >> >> A code revision. > > How do you become aware of a broken contract? > Statically? Dynamically? Me? I am not a part of the system. These terms do not apply to me. Before going any further, you should define the system under consideration. Note that your "DbC mindset" includes the programmer(s) into the system, delivered and deployed. Isn't that indicatory? (:-)) >>> I'm a programmer. If I "design" anything, it is a program whose >>> parts need to interact in a way that meets some almost entirely >>> non-mathematical specification. >> >> Mathematics has nothing to do with this. It is about a clear distinction >> between a contract and a condition, how undesirable it could be but >> nevertheless it is a condition, which you, as a programmer are obliged to >> consider as *possible*. Eiffel gives you an illusion of safety. > > No. Eiffel marketing claims that a fully proven DbC program > is 100% bug free. I can imagine Microsoft marketing doing same, if they didn't already... >> Simply consider >> the following rule: my program shall handle each exception I introduce. >> Objections? > > No objection. > >> Then consider exceptions from assertions. > > That is what Eiffel's rescue mechanism is about. And how do you rescue from: function "-" (X : Positive) return Positive; Note, if you handle an exception then it is same as if-statement. (I agree that if-statements could be better arranged, have nicer syntax etc. Is that the essence of Eiffel's DbC?) >>>>> How would you specify >>>>> >>>>> subtype Even is ...; ? >>>> >>>> Ada's syntax is: >>>> >>>> subtype<name> is<name> <constraint>; >>> >>> What will static<name> and static<constraint> be for subtype Even? >> >> No, in Ada<constraint> is not required to be static. Example: >> >> procedure F (A : String) is >> subtype Span is Integer range A'Range; > > Is the constraint, not to be static, then part of the contractual > specification of subtype Even? The specification of includes all possible values of the constraint. When you assign -1 to Positive, it is not an error, it is a valid, well-defined program, which behavior is required to be Constraint_Error propagation. When you assign -1.0 to Positive, it is an error and the program is invalid. Where and how you are using these two mechanisms is up to you. A FORTRAN program can be written in Ada, of course... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-13 8:39 ` Dmitry A. Kazakov @ 2010-05-14 23:45 ` Georg Bauhaus 2010-05-15 9:30 ` Dmitry A. Kazakov 0 siblings, 1 reply; 95+ messages in thread From: Georg Bauhaus @ 2010-05-14 23:45 UTC (permalink / raw) On 5/13/10 10:39 AM, Dmitry A. Kazakov wrote: >> Ada seems better here. But before the arrival of preconditions >> etc. Ada didn't have that much to offer to programmers wanting >> to state sets of permissible values, for example for subprogram >> parameters. > > Ada has strong types. "A set of permissible values" does not look like > that. Ada's strong types are not really strong enough to express a supplier library's ADT expectations in the sense of DbC. Subtypes (or the type system) would need to by more specific for that. One OOSC2 example is easily handled by Ada's subtypes, though. It also shows that DbC does *not* assume contracts should necessarily become a meaningful part of your executing program, i.e. have the program do assertion monitoring. On the contrary. function sqrt(x: REAL) return REAL; pragma Precondition (X >= 0.0); -- and something like pragma --- Postcondition (sqrt'Result * sqrt'Result = x); function Sqrt(x: REAL) return REAL is begin ... end Sqrt; (The requirement that X >= 0.0 on entry will actually be part of a translated *Ada* program if REAL above is defined as a subtype of some type that includes values below 0.0. The check is not necessarily part of a corresponding Eiffel program that has require X >= 0.0.) Anyway, wherever the Ada compiler sees that a value passed to Sqrt is < 0.0, it can warn at least. The following would *not* be a DbC style Sqrt: function Sqrt_Not_DbC (X: REAL) return REAL is begin if X < 0.0 then -- "Handle the error, somehow" else -- "Proceed with normal square root computation" end if; end Sqrt_Not_DbC; -- cf. OOSC2, p.343 Instead, supplier is supposed to write the program Sqrt as if X >= 0.0 on entry. Only if X >= 0.0 can client legitimately expect supplier's Sqrt to terminate in a state that satisfies the postcondition and INV. (INV is probably just True here.) >> Ada subtypes, e.g. scalars, are poorly equipped for this style of >> value set specification, AFAICS. They do establish two implicit >> preconditions (>= S'First and<= S'Last). > > These are not preconditions, but invariants. 'First and 'Last are invariants of the type and they express preconditions when reinterpreted in the normal DbC way. Again, can you produce a statically checked invariant for subtype Even? >> package P is >> >> type Number is range 1 .. 10; >> function Compute (A, B: Number) return Number >> with Precondition => A>= B; > > I don't understand this notation. It says that the client of Compute would have to provide A, B such that A >= B if client expects Compute to produce its postcondition; otherwise, the expectation is unjustified and Compute is not bound by the contract, i.e. may fail and produce whatever, including an exception. The contract here is this: I, client, give you, Compute, numbers A and B that are as you told me. I, Compute, will produce my Postcondition if you give me numbers A and B as I told you. > I do not accept "preconditions" in the operations, which are not statically > true: That's your choice then, but not DbC's, which is more inclusive (again, statically checked subtype Even vs. X rem 2 = 0). > function "/" (X, Y : Number) return Number -- Wrong! > pre : Y /= 0.0; > > function "/" (X, Y : Number) return Number -- Right! > post : result = X/Y or else Constraint_Error; The second "/" is a DbC one. There is a big warning sign in OOSC2 that says, / \ NO PRECONDITION TOO BIG OR TOO SMALL \ / While a matter of choice, there is one strict rule: "It is _never_ acceptable to deal with a correctness condition on both the client and supplier sides." >>>> Which set of "specifications" has only static things in it? >>>> Why exclude conditionals whose results cannot reasonably >>>> be computed by the compiler but >>>> >>>> (a) can be computed for every single case occuring in the >>>> executing program >>> >>> If they can for *every* case, they are statically checkable, per >>> definition. >> >> "Every case" cannot "reasonably be computed by the compiler". > > Either they can or cannot. You said they can, but then added "unreasonably > can", or "reasonably cannot", whatever. Sound like Eiffel's contracts, x > is even, not really even, we wanted it be even... (:-)) When I mentioned "not reasonably be computed by the compiler" early on, I meant that DbC should be a possible system that helps programmers. I did not want to theorize program analysis systems that are impossible to produce. I can think of a DbC program with assertion monitoring turned on and see it as a stepwise attempt at working out the correctness properties of the program. For example, I can see the program crash when a new change set makes some variable have a different value. This value no longer meets the stated requirements of some subprogram. That is shown then by the run-time and I can think again. Preferrably think about possible mistakes in my attempts at corectness lemmata, since otherwise this procedure will degrade into debugging things into some state. But DbC here yields more than dealing with exceptions and erroneous execution in some random fashion can possibly achieve! >>>> (b) can guide the author of a client of a DbC component? >>> >>> I don't know what does it mean technically. >> >> Contractually, it means "do as the preconditions say." > > Like "do as comments say"? Yes. Only, a DbC system can be quite helpful in checking my understanding of more formal "comments". > Note, since your "preconditions" are not static, > how can you know *what* they say, in order to do as they do? I can write my client code such that the preconditions are true. I know what a procondition says if I do not need to solve hard problems to know the meaning of a predicate. Note that DbC includes requirements that are stated in natural language. Of course, not even trying to write predicates defeats the purpose of contracting between client and supplier, assisted by the DbC system. E.g., I read a number from input, and another number from input. I know that subprogram P wants one number to be odd and the other number to be even. (Otherwise, it does not guarantee that it produces its postcondition.) These are easily tested conditions. I know what I have to test and I know how to test what. >> IOW, no redundant checks. > > No, it would be *inconsistent* checks. No program can check itself. DbC checks are not part of the (intended) program. Monitoring can be turned off and this should have no effect on program correctness. The proof obligation rests on us, the programmers. >>>> For example, assume that Is_Prime(N) is a precondition of sub P. >>>> Furthermore, TIME(Is_Prime(N))>> PERMISSIBLE_TIME. >>>> Then, still, PRE: Is_Prime (N) expresses an obligation, >>>> part of a contract: Don't call P unless N is prime, >>>> no matter whether or not assertion checking is in effect. >>> >>> char X [80]; // Don't use X[80], X[81], no matter etc. >> >> Yes, and don't use X[-200]. But you can. OTOH: >> >> function Access_Element (S: String_80; X: Index_80); >> >> function Careful (S: String_80; X: Index_80) >> with Precondition => X rem 2 = 1; >> >> How would you write a statically checked version? > > Trivially: > > function Careful (S: String_80; X: Index_80) > with Precondition True; > with Postcondition<whatever> or Constraint_Error This is legitimate I'd say, but is also is a destructive omission of what the precondition above does specify. Yours (True) does not tell the client programmer the conditions that by DbC will guarantee Postcondition. Without hardware failure or other occurrences that cannot be expected to be handled by the Careful algorithm, Careful must produce Postcondition provided odd Index_80 numbers are passed for X. But in your version, (a) there is nothing the programmer knows about valid Index_80 values (viz. the odd ones) (b) there is no debugging hook that can be turned on or off (monitoring the precondition X rem 2 = 1). > other things you mentioned are control flow control statements. It is > really simply: an error/correctness check is a statement about the program > behavior. If-statement/exception etc is the program behavior. Normal If-statements and exceptions cannot be turned off. > Note > that your "DbC mindset" includes the programmer(s) into the system, > delivered and deployed. Isn't that indicatory? (:-)) The programmer is the one ingredient that matters most in DbC, since programming is a human activity, and contracts are between clients and suppliers of software components (classes). > And how do you rescue from: > > function "-" (X : Positive) return Positive; > > Note, if you handle an exception then it is same as if-statement. (I agree > that if-statements could be better arranged, have nicer syntax etc. Is that > the essence of Eiffel's DbC?) I'm assuming this is not an input-sanitizing function. You don't handle the exception as part of the algorithm: minus: INTEGER require Current > 1 do Current := Current - 1 end ensure Current + 1 = old Current Where Ada requires "ifs" for bounds checking and raising an exception accordingly, DbC/Eiffel requires that you express the correctness properties of subprograms *and* that you choose whether or not you want the "if", and which ones. >>>>>> How would you specify >>>>>> >>>>>> subtype Even is ...; ? >>>>> >>>>> Ada's syntax is: >>>>> >>>>> subtype<name> is<name> <constraint>; >>>> >>>> What will static<name> and static<constraint> be for subtype Even? >>> >>> No, in Ada<constraint> is not required to be static. Example: >>> >>> procedure F (A : String) is >>> subtype Span is Integer range A'Range; >> >> Is the constraint, not to be static, then part of the contractual >> specification of subtype Even? > > The specification of includes all possible values of the constraint. When > you assign -1 to Positive, it is not an error, it is a valid, well-defined > program, which behavior is required to be Constraint_Error propagation. > When you assign -1.0 to Positive, it is an error and the program is > invalid. Where and how you are using these two mechanisms is up to you. A > FORTRAN program can be written in Ada, of course... > This specifies that assigning -1 to a positive will raise an exception. It does not specify the possible values for Even (which would be constrained to include only even numbers). ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-14 23:45 ` Georg Bauhaus @ 2010-05-15 9:30 ` Dmitry A. Kazakov 2010-05-15 18:39 ` Georg Bauhaus 0 siblings, 1 reply; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-15 9:30 UTC (permalink / raw) On Sat, 15 May 2010 01:45:50 +0200, Georg Bauhaus wrote: > On 5/13/10 10:39 AM, Dmitry A. Kazakov wrote: > >>> Ada seems better here. But before the arrival of preconditions >>> etc. Ada didn't have that much to offer to programmers wanting >>> to state sets of permissible values, for example for subprogram >>> parameters. >> >> Ada has strong types. "A set of permissible values" does not look like >> that. > > Ada's strong types are not really strong enough to express > a supplier library's ADT expectations in the sense of DbC. No type system can express the program semantics. Otherwise you would need not program any bodies, only declarations. > Again, can you produce a statically checked invariant for > subtype Even? Yes, I can: type Even is private; -- No literals visible function To_Integer (X : Even) return Integer; function To_Even (X : Integer) return Even; private type Even is new Integer; -- Use literals as follows: 1 means 2 function To_Integer (X : Even) return Integer is begin return Integer (X * 2); end To_Integer; function To_Even (X : Integer) return Even is begin if X mod 2 = 0 then return Even (X / 2); else raise Constraint_Error; end if; end To_Even; >>> package P is >>> >>> type Number is range 1 .. 10; >>> function Compute (A, B: Number) return Number >>> with Precondition => A>= B; >> >> I don't understand this notation. > > It says that the client of Compute would have to provide > A, B such that A >= B if client expects Compute to produce > its postcondition; otherwise, Compute should have the contract: if the sequence A,B is sorted then ... else Constraint_Error propagated. And of course, A, B is just an interval [B, A], and should be declared as such: function Compute (X : Interval) return Number with Precondition => True; > Yes. Only, a DbC system can be quite helpful in checking > my understanding of more formal "comments". You say that Eiffel DbC is about writing structured comments? I do not object. >> Note, since your "preconditions" are not static, >> how can you know *what* they say, in order to do as they do? > > I can write my client code such that the preconditions are > true. Really? What about: pre : not HALT(p) There is a reason why they aren't static. >>> IOW, no redundant checks. >> >> No, it would be *inconsistent* checks. No program can check itself. > > DbC checks are not part of the (intended) program. Monitoring can be > turned off and this should have no effect on program correctness. and thus on program execution. q.e.d. >> Trivially: >> >> function Careful (S: String_80; X: Index_80) >> with Precondition True; >> with Postcondition<whatever> or Constraint_Error > > This is legitimate I'd say, but is also is a destructive omission of > what the precondition above does specify. Yours (True) does not tell > the client programmer the conditions that by DbC will guarantee > Postcondition. Without hardware failure or other occurrences > that cannot be expected to be handled by the Careful algorithm, > Careful must produce Postcondition provided odd Index_80 numbers > are passed for X. But in your version, > > (a) there is nothing the programmer knows about valid Index_80 > values (viz. the odd ones) They are *all* valid, that is the contract of Careful. > (b) there is no debugging hook that can be turned on > or off (monitoring the precondition X rem 2 = 1). Debugging hooks do not belong to code. >> other things you mentioned are control flow control statements. It is >> really simply: an error/correctness check is a statement about the program >> behavior. If-statement/exception etc is the program behavior. > > Normal If-statements and exceptions cannot be turned off. Come on. C has preprocessor! >> Note >> that your "DbC mindset" includes the programmer(s) into the system, >> delivered and deployed. Isn't that indicatory? (:-)) > > The programmer is the one ingredient that matters most in DbC, > since programming is a human activity, and contracts are between > clients and suppliers of software components (classes). That is what your car manufacturer will tell you next time, when the brake system will accelerate instead of braking... >> And how do you rescue from: >> >> function "-" (X : Positive) return Positive; >> >> Note, if you handle an exception then it is same as if-statement. (I agree >> that if-statements could be better arranged, have nicer syntax etc. Is that >> the essence of Eiffel's DbC?) > > I'm assuming this is not an input-sanitizing function. It was unary minus. > Where Ada requires "ifs" for bounds checking and raising an > exception accordingly, DbC/Eiffel requires that you express the > correctness properties of subprograms *and* that you choose > whether or not you want the "if", and which ones. Bounds are one kind of constraints. Eiffel has more of those. Ada goes in the same direction as Robert's response shows. I don't like it for two reasons: 1. Dynamic checks. This was discussed. Correctness checks shall be static, else it is a part of the behavior to be contracted as any other. 2. It is weakly/un-typed. The constraints you impose on input and output are specifications of a [sub]type. 2.a. This type is anonymous 2.b. This type mutates (precondition /= postcondition) 2.c. This type is inferred and structurally equivalent To me this is a deep breach with the core of Ada type system. > This specifies that assigning -1 to a positive will raise an exception. > It does not specify the possible values for Even (which would be > constrained to include only even numbers). You have to define "possible value": 1. Member of the type domain set. (3 is a member of the Even as a subtype of Integer) 2. Value of an initialized instance (3 cannot be a value of any Even object) (Considering Even an Ada subtype or a type inheriting to integer.) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-15 9:30 ` Dmitry A. Kazakov @ 2010-05-15 18:39 ` Georg Bauhaus 2010-05-15 20:33 ` Dmitry A. Kazakov 0 siblings, 1 reply; 95+ messages in thread From: Georg Bauhaus @ 2010-05-15 18:39 UTC (permalink / raw) On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote: > No type system can express the program semantics. OK, lets keep this in mind. > Compute should have the contract: if the sequence A,B is sorted then ... > else Constraint_Error propagated. And of course, A, B is just an interval > [B, A], and should be declared as such: > > function Compute (X : Interval) return Number > with Precondition => True; OK, I guess we'd have a To_Interval (A, B) function raising constraint_error in case the programmer improperly passes A < B. Which he has learned not to do from some comment that states contractual obligations of client wishing to call To_Interval? >>> Note, since your "preconditions" are not static, >>> how can you know *what* they say, in order to do as they do? >> >> I can write my client code such that the preconditions are >> true. > > Really? What about: > > pre : not HALT(p) This is why I mentioned "not solve hard problems". I want to keep making sense in my preconditions/comments. > There is a reason why they aren't static. Practically, yes, there is a reason why normal programming cannot hope to rely on static analysis. >>>> IOW, no redundant checks. >>> >>> No, it would be *inconsistent* checks. No program can check itself. >> >> DbC checks are not part of the (intended) program. Monitoring can be >> turned off and this should have no effect on program correctness. > > and thus on program execution. q.e.d. The programs (with or without monitoring) are not too different and hence will lead to a useful program construction process. (Better exceptions.) >> (a) there is nothing the programmer knows about valid Index_80 >> values (viz. the odd ones) > > They are *all* valid, that is the contract of Careful. I guess we disagree here: I think that a "programming into exceptions" style leads to the universally applicable precondition True, but otherwise keeps the programmer in the dark about how to not make a subprogram raise. OTOH, being more specific (trying to explain additional "constraints") seems helpful. Here I recall "No type system can express the program semantics." Until Ada has a type system that can express expectations better than predicates, I'll rather have stupid, weakly typed predicates, supported by tools, than nothing. loop begin P(X); exit; exception when constraint_error => X := find_another_x; end; end loop; >> (b) there is no debugging hook that can be turned on >> or off (monitoring the precondition X rem 2 = 1). > > Debugging hooks do not belong to code. I guess my wording was too unspecific. Call it tracing automatism or whatever. > You have to define "possible value": In the sense of DbC: values that client can pass without violating the DbC contract. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-15 18:39 ` Georg Bauhaus @ 2010-05-15 20:33 ` Dmitry A. Kazakov 0 siblings, 0 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-15 20:33 UTC (permalink / raw) On Sat, 15 May 2010 20:39:46 +0200, Georg Bauhaus wrote: > On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote: > >> Compute should have the contract: if the sequence A,B is sorted then ... >> else Constraint_Error propagated. And of course, A, B is just an interval >> [B, A], and should be declared as such: >> >> function Compute (X : Interval) return Number >> with Precondition => True; > > OK, I guess we'd have a To_Interval (A, B) function raising > constraint_error in case the programmer improperly passes A < B. > Which he has learned not to do from some comment that states > contractual obligations of client wishing to call To_Interval? He learned that from the semantics of intervals, when he uses intervals he supposed to know what they are. When you write a precondition you use some premises. Consider primitive operations of the type T. You cannot describe T in terms of T. I.e. + cannot refer to +. So interval must be known to the programmer. >> There is a reason why they aren't static. > > Practically, yes, there is a reason why normal programming > cannot hope to rely on static analysis. If it could, you would not need program anything. E.g. the result would be obtained statically. >>>>> IOW, no redundant checks. >>>> >>>> No, it would be *inconsistent* checks. No program can check itself. >>> >>> DbC checks are not part of the (intended) program. Monitoring can be >>> turned off and this should have no effect on program correctness. >> >> and thus on program execution. q.e.d. > > The programs (with or without monitoring) are not too different > and hence will lead to a useful program construction process. How do you measure the difference? >>> (a) there is nothing the programmer knows about valid Index_80 >>> values (viz. the odd ones) >> >> They are *all* valid, that is the contract of Careful. > > I guess we disagree here: I think that a "programming into > exceptions" style leads to the universally applicable precondition > True, but otherwise keeps the programmer in the dark about > how to not make a subprogram raise. This is what programming in Ada all about. Since the rest of the language is by large safe, the main problem is debugging exceptions. I would like Ada having contracted exceptions rather than run-time assertions producing more exceptions than we already have. >>> (b) there is no debugging hook that can be turned on >>> or off (monitoring the precondition X rem 2 = 1). >> >> Debugging hooks do not belong to code. > > I guess my wording was too unspecific. Call it tracing > automatism or whatever. Nope, the key feature of tracing is that it does not change the program's behavior. Assertions with handled exceptions do change it. It is a very poor debugging tool. I would prefer a decent debugger to run-time assertions. Make it remember the break conditions between runs. That would be helpful and consistent. >> You have to define "possible value": > > In the sense of DbC: values that client can pass without > violating the DbC contract. And contract is of course a predicate of that set of values? Nice circular definitions. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 18:09 ` Georg Bauhaus 2010-05-12 18:33 ` Dmitry A. Kazakov @ 2010-05-15 0:17 ` Robert A Duff 2010-05-15 9:40 ` Dmitry A. Kazakov 1 sibling, 1 reply; 95+ messages in thread From: Robert A Duff @ 2010-05-15 0:17 UTC (permalink / raw) Georg Bauhaus <rm.dash-bauhaus@futureapps.de> writes: > How would you specify > > subtype Even is ...; ? In Ada 2012, if AI-153 gets approved, you will be able to say: subtype Even is Integer with Predicate => (Even mod 2) = 0; ^^^^ refers to the "current instance" of the subtype That particular example isn't very useful, but this kind of thing is: type Color is (Red, Orange, Yellow, Green, Blue); subtype Primary_Color is Color with Predicate => Primary_Color in (Red, Green, Blue); By the way, I don't think "static" is a property of assertions. It's a property of how they're checked. If we have a precondition that "X > Y" (where X and Y are formal parameters), that's neither "static" nor "dynamic" in and of itself. One tool (e.g. an Ada compiler) might check it dynamically. A smarter tool (a proof checker, or a smarter compiler, or even a human being) might check it statically. It might even be checked statically at some call sites, but not others. - Bob ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-15 0:17 ` Robert A Duff @ 2010-05-15 9:40 ` Dmitry A. Kazakov 0 siblings, 0 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-15 9:40 UTC (permalink / raw) On Fri, 14 May 2010 20:17:30 -0400, Robert A Duff wrote: > By the way, I don't think "static" is a property of assertions. > It's a property of how they're checked. If we have > a precondition that "X > Y" (where X and Y are formal parameters), > that's neither "static" nor "dynamic" in and of itself. It becomes static or dynamic when you define of which language the formula "X > Y" is. If it is of the "language of Ada bodies," e.g. compiled into a run-time code, then it is dynamic. If it is of the "language of Ada specifications" (compiled into compiler messages), then it is static. Ada, at least in its earlier years, tried to segregate these. > One tool (e.g. an Ada compiler) might check it dynamically. That would be true C... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 17:24 ` Dmitry A. Kazakov 2010-05-12 18:09 ` Georg Bauhaus @ 2010-05-12 18:15 ` Georg Bauhaus 2010-05-25 20:45 ` Yannick Duchêne (Hibou57) 2 siblings, 0 replies; 95+ messages in thread From: Georg Bauhaus @ 2010-05-12 18:15 UTC (permalink / raw) On 12.05.10 19:24, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: > >> 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 better >> to catch error the sooner and understand why this was an error. > > 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. Another important difference between a simple "if" and DbC assertions: The routine conditions must be consistent along the inheritance chain. It seems silly to have the programmer walk up and down the chain and make sure that substitutability isn't violated by manual "if" style preconditions. Hence, Eiffel's require else and ensure then for overriding routines. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 17:24 ` Dmitry A. Kazakov 2010-05-12 18:09 ` Georg Bauhaus 2010-05-12 18:15 ` Georg Bauhaus @ 2010-05-25 20:45 ` Yannick Duchêne (Hibou57) 2010-05-26 7:55 ` Dmitry A. Kazakov 2010-05-26 8:38 ` stefan-lucks 2 siblings, 2 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-25 20:45 UTC (permalink / raw) Le Wed, 12 May 2010 19:24:11 +0200, Dmitry A. Kazakov <mailbox@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. 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. -- There is even better than a pragma Assert: a SPARK --# check. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-25 20:45 ` Yannick Duchêne (Hibou57) @ 2010-05-26 7:55 ` Dmitry A. Kazakov 2010-05-26 8:38 ` stefan-lucks 1 sibling, 0 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-26 7:55 UTC (permalink / raw) 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@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 ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-25 20:45 ` Yannick Duchêne (Hibou57) 2010-05-26 7:55 ` Dmitry A. Kazakov @ 2010-05-26 8:38 ` stefan-lucks 2010-05-26 8:01 ` Yannick Duchêne (Hibou57) 2010-05-26 11:25 ` Yannick Duchêne (Hibou57) 1 sibling, 2 replies; 95+ messages in thread From: stefan-lucks @ 2010-05-26 8:38 UTC (permalink / raw) [-- Attachment #1: Type: TEXT/PLAIN, Size: 1395 bytes --] 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! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 8:38 ` stefan-lucks @ 2010-05-26 8:01 ` Yannick Duchêne (Hibou57) 2010-05-26 11:25 ` Yannick Duchêne (Hibou57) 1 sibling, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-26 8:01 UTC (permalink / raw) Le Wed, 26 May 2010 10:38:20 +0200, <stefan-lucks@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. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 8:38 ` stefan-lucks 2010-05-26 8:01 ` Yannick Duchêne (Hibou57) @ 2010-05-26 11:25 ` Yannick Duchêne (Hibou57) 2010-05-26 13:02 ` stefan-lucks 1 sibling, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-26 11:25 UTC (permalink / raw) Le Wed, 26 May 2010 10:38:20 +0200, <stefan-lucks@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. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 11:25 ` Yannick Duchêne (Hibou57) @ 2010-05-26 13:02 ` stefan-lucks 2010-05-26 12:22 ` Yannick Duchêne (Hibou57) 2010-05-26 13:06 ` (see below) 0 siblings, 2 replies; 95+ messages in thread From: stefan-lucks @ 2010-05-26 13:02 UTC (permalink / raw) [-- Attachment #1: Type: TEXT/PLAIN, Size: 1133 bytes --] 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! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 13:02 ` stefan-lucks @ 2010-05-26 12:22 ` Yannick Duchêne (Hibou57) 2010-05-27 12:47 ` stefan-lucks 2010-05-26 13:06 ` (see below) 1 sibling, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-26 12:22 UTC (permalink / raw) Le Wed, 26 May 2010 15:02:50 +0200, <stefan-lucks@see-the.signature> a écrit: > 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. This is just notation, no one can infer anything from such a premise. > 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. For perception, this matter, I agree. -- There is even better than a pragma Assert: a SPARK --# check. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 12:22 ` Yannick Duchêne (Hibou57) @ 2010-05-27 12:47 ` stefan-lucks 2010-05-27 12:26 ` Yannick Duchêne (Hibou57) 0 siblings, 1 reply; 95+ messages in thread From: stefan-lucks @ 2010-05-27 12:47 UTC (permalink / raw) [-- Attachment #1: Type: TEXT/PLAIN, Size: 1391 bytes --] On Wed, 26 May 2010, Yannick Duch�ne (Hibou57) wrote: > Le Wed, 26 May 2010 15:02:50 +0200, <stefan-lucks@see-the.signature> a �crit: > >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. > This is just notation, no one can infer anything from such a premise. Notation is not such unimportant. And this is a bit more than just notation: You use different *tools* to compile the program-while-ignoring-all-annotations and to check the additional information provided by the annotations. This means, that psychologically the information in the annotations appears to be the "less important" stuff. E.g., a badly flawed SPARK program may still be compiled by an Ada compiler, but a syntactically incorrect Ada-program will be found flawed by the SPARK tools. > [...] For perception, this matter, I agree. See! -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-27 12:47 ` stefan-lucks @ 2010-05-27 12:26 ` Yannick Duchêne (Hibou57) 0 siblings, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-27 12:26 UTC (permalink / raw) Le Thu, 27 May 2010 14:47:15 +0200, <stefan-lucks@see-the.signature> a écrit: > Notation is not such unimportant. > > And this is a bit more than just notation: You use different *tools* to > compile the program-while-ignoring-all-annotations and to check the > additional information provided by the annotations. This means, that > psychologically the information in the annotations appears to be the > "less > important" stuff. Do not make this a rule, as this depends on one's expectations (so receptivity to that what looks like his/her expectations). One who wish and expect what belongs to these annotations, will see these as important things. One who does not expect these annotations and may perhaps even wish that would not exist (like a student working on an assignment) will see these as non so much important. This is a matter of receptivity. I was a bit wrong (did a shortcut) when I suggested “this is just annotation”, as I agree the form of an annotation is important for readability. > E.g., a badly flawed SPARK program may still be compiled > by an Ada compiler, Yes > but a syntactically incorrect Ada-program will be > found flawed by the SPARK tools. Not a rule, as not all notations oriented language may check every thing of the host language. SPARK does, but I'm pretty sure not all do (I think we were talking about the general case here, not only about the SPARK special case). -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 13:02 ` stefan-lucks 2010-05-26 12:22 ` Yannick Duchêne (Hibou57) @ 2010-05-26 13:06 ` (see below) 2010-05-27 12:41 ` stefan-lucks 1 sibling, 1 reply; 95+ messages in thread From: (see below) @ 2010-05-26 13:06 UTC (permalink / raw) On 26/05/2010 14:02, in article Pine.LNX.4.64.1005261455260.26620@medsec1.medien.uni-weimar.de, "stefan-lucks@see-the.signature" <stefan-lucks@see-the.signature> wrote: > 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. > Why? -- Bill Findlay <surname><forename> chez blueyonder.co.uk ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-26 13:06 ` (see below) @ 2010-05-27 12:41 ` stefan-lucks 2010-05-27 12:29 ` Yannick Duchêne (Hibou57) 2010-05-27 15:21 ` (see below) 0 siblings, 2 replies; 95+ messages in thread From: stefan-lucks @ 2010-05-27 12:41 UTC (permalink / raw) On Wed, 26 May 2010, (see below) wrote: > On 26/05/2010 14:02, in article > Pine.LNX.4.64.1005261455260.26620@medsec1.medien.uni-weimar.de, > "stefan-lucks@see-the.signature" <stefan-lucks@see-the.signature> wrote: > > > I am a university teacher. For me, it makes quite a difference if I either > > explain students one coherent language where contracts are an integral part > > of (like Eiffel), or one programming language plus an additional language > > for the annotations. > > > > Why? Because students appreciate coherent concepts. More specifically: There is a syntactic gap between SPARK and Ada. I had given a course on Ada and SPARK recently, and my students seem to be permanently tempted to focus on the Ada-part, while contracts and proofs where considered a more "optional" add-on, rather than a necessary and integral part of their work. Beware: My students are some of the people who will write the software you will use tomorrow. ;-) -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-27 12:41 ` stefan-lucks @ 2010-05-27 12:29 ` Yannick Duchêne (Hibou57) 2010-05-27 15:21 ` (see below) 1 sibling, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-27 12:29 UTC (permalink / raw) Le Thu, 27 May 2010 14:41:58 +0200, <stefan-lucks@see-the.signature> a écrit: > Because students appreciate coherent concepts. > > More specifically: There is a syntactic gap between SPARK and Ada. I had > given a course on Ada and SPARK recently, and my students seem to be > permanently tempted to focus on the Ada-part, while contracts and proofs > where considered a more "optional" add-on, rather than a necessary and > integral part of their work. I see, and I believe this question is close to a kind of ergonomic matter (there is something like ergonomy in languages too). -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-27 12:41 ` stefan-lucks 2010-05-27 12:29 ` Yannick Duchêne (Hibou57) @ 2010-05-27 15:21 ` (see below) 2010-06-03 3:16 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: (see below) @ 2010-05-27 15:21 UTC (permalink / raw) On 27/05/2010 13:41, in article Pine.LNX.4.64.1005271422490.30605@medsec1.medien.uni-weimar.de, "stefan-lucks@see-the.signature" <stefan-lucks@see-the.signature> wrote: > On Wed, 26 May 2010, (see below) wrote: > >> On 26/05/2010 14:02, in article >> Pine.LNX.4.64.1005261455260.26620@medsec1.medien.uni-weimar.de, >> "stefan-lucks@see-the.signature" <stefan-lucks@see-the.signature> wrote: >> >>> I am a university teacher. For me, it makes quite a difference if I either >>> explain students one coherent language where contracts are an integral part >>> of (like Eiffel), or one programming language plus an additional language >>> for the annotations. >>> >> >> Why? > > Because students appreciate coherent concepts. But concepts /= language notations. > More specifically: There is a syntactic gap between SPARK and Ada. I had > given a course on Ada and SPARK recently, and my students seem to be > permanently tempted to focus on the Ada-part, while contracts and proofs > where considered a more "optional" add-on, rather than a necessary and > integral part of their work. Is that an inaccurate perception? SPARK contracts and proofs ARE add-ons. My experience is that CS/SE students always focus on "coding" at the expense of problem analysis, program design, project planning, verification, validation, documentation, and anything else they find less congenial. I doubt that the SPARK notation has much to do with that. > > Beware: My students are some of the people who will > write the software you will use tomorrow. ;-) Since they are learning SPARK/Ada I am less worried by that than I might otherwise have been. 8-) Beware: My ex-students are some of the people who wrote the software you are using today. ;-) -- Bill Findlay <surname><forename> chez blueyonder.co.uk ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-27 15:21 ` (see below) @ 2010-06-03 3:16 ` Yannick Duchêne (Hibou57) 2010-06-03 10:42 ` Brian Drummond 2010-06-03 13:49 ` (see below) 0 siblings, 2 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-06-03 3:16 UTC (permalink / raw) Le Thu, 27 May 2010 17:21:57 +0200, (see below) <yaldnif.w@blueyonder.co.uk> a écrit: > My experience is that CS/SE students always focus on "coding" at the > expense > of problem analysis, program design, project planning, verification, > validation, documentation, and anything else they find less congenial. I always though this was not so much with these students. So why do they choose it if they are not aware of what it requires ? > Beware: My ex-students are some of the people who > wrote the software you are using today. ;-) > You're teacher too like Stefan ? -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-03 3:16 ` Yannick Duchêne (Hibou57) @ 2010-06-03 10:42 ` Brian Drummond 2010-06-03 21:14 ` (see below) 2010-06-03 13:49 ` (see below) 1 sibling, 1 reply; 95+ messages in thread From: Brian Drummond @ 2010-06-03 10:42 UTC (permalink / raw) On Thu, 03 Jun 2010 05:16:14 +0200, Yannick Duch�ne (Hibou57) <yannick_duchene@yahoo.fr> wrote: >Le Thu, 27 May 2010 17:21:57 +0200, (see below) ><yaldnif.w@blueyonder.co.uk> a �crit: >> My experience is that CS/SE students always focus on "coding" at the >> expense >> of problem analysis, program design, project planning, verification, >> validation, documentation, and anything else they find less congenial. >I always though this was not so much with these students. So why do they >choose it if they are not aware of what it requires ? > >> Beware: My ex-students are some of the people who >> wrote the software you are using today. ;-) >> >You're teacher too like Stefan ? If you learned Pascal, there's a pretty good chance you learned it from his book... http://www.amazon.co.uk/PASCAL-Introduction-Methodical-Programming-Instructions/dp/0273021885/ref=sr_1_1?ie=UTF8&s=books&qid=1275561327&sr=1-1 - Brian ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-03 10:42 ` Brian Drummond @ 2010-06-03 21:14 ` (see below) 2010-06-03 22:00 ` Britt Snodgrass 0 siblings, 1 reply; 95+ messages in thread From: (see below) @ 2010-06-03 21:14 UTC (permalink / raw) On 03/06/2010 11:42, in article 8k1f06t4uc0t319t9v6t3als2ifu5evbku@4ax.com, "Brian Drummond" <brian_drummond@btconnect.com> wrote: > On Thu, 03 Jun 2010 05:16:14 +0200, Yannick Duch�ne (Hibou57) > <yannick_duchene@yahoo.fr> wrote: > >> Le Thu, 27 May 2010 17:21:57 +0200, (see below) >> <yaldnif.w@blueyonder.co.uk> a �crit: >>> My experience is that CS/SE students always focus on "coding" at the >>> expense >>> of problem analysis, program design, project planning, verification, >>> validation, documentation, and anything else they find less congenial. >> I always though this was not so much with these students. So why do they >> choose it if they are not aware of what it requires ? >> >>> Beware: My ex-students are some of the people who >>> wrote the software you are using today. ;-) >>> >> You're teacher too like Stefan ? > > If you learned Pascal, there's a pretty good chance you learned it from > his book... > > http://www.amazon.co.uk/PASCAL-Introduction-Methodical-Programming-Instruction > s/dp/0273021885/ref=sr_1_1?ie=UTF8&s=books&qid=1275561327&sr=1-1 I much prefer: <http://www.amazon.co.uk/ADA-Language-Methodology-International-Computing/dp /0130040789/ref=sr_1_1?ie=UTF8&s=books&qid=1275599490&sr=1-1> But it did not sell nearly as well, despite the complimentary foreword by C.A.R. Hoare 8-) -- Bill Findlay <surname><forename> chez blueyonder.co.uk ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-03 21:14 ` (see below) @ 2010-06-03 22:00 ` Britt Snodgrass 2010-06-03 22:29 ` (see below) 0 siblings, 1 reply; 95+ messages in thread From: Britt Snodgrass @ 2010-06-03 22:00 UTC (permalink / raw) On Jun 3, 4:14 pm, "(see below)" <yaldni...@blueyonder.co.uk> wrote: > On 03/06/2010 11:42, in article 8k1f06t4uc0t319t9v6t3als2ifu5ev...@4ax.com, > > I much prefer: > > <http://www.amazon.co.uk/ADA-Language-Methodology-International-Comput...> > > But it did not sell nearly as well, despite the complimentary foreword by > C.A.R. Hoare 8-) > Potential buyers may have been put off by the miscapitilization ("ADA") of Ada on the front cover. I don't know why several publishers of Ada books made that mistake. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-03 22:00 ` Britt Snodgrass @ 2010-06-03 22:29 ` (see below) 0 siblings, 0 replies; 95+ messages in thread From: (see below) @ 2010-06-03 22:29 UTC (permalink / raw) On 03/06/2010 23:00, in article d361037e-1d7b-4beb-8f45-1b762afc813f@k39g2000yqb.googlegroups.com, "Britt Snodgrass" <britt.snodgrass@gmail.com> wrote: > On Jun 3, 4:14�pm, "(see below)" <yaldni...@blueyonder.co.uk> wrote: >> On 03/06/2010 11:42, in article 8k1f06t4uc0t319t9v6t3als2ifu5ev...@4ax.com, >> > >> I much prefer: >> >> <http://www.amazon.co.uk/ADA-Language-Methodology-International-Comput...> >> >> But it did not sell nearly as well, despite the complimentary foreword by >> C.A.R. Hoare 8-) >> > > Potential buyers may have been put off by the miscapitilization I doubt that. People have to be inducted into the cult before they start worrying about capitalization. 8-) > ("ADA") of Ada on the front cover. I don't know why several > publishers of Ada books made that mistake. Publishers move in mysterious ways their "wonders" to perform. [That is the polite version of what I think of them. 8-( ] -- Bill Findlay <surname><forename> chez blueyonder.co.uk ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-03 3:16 ` Yannick Duchêne (Hibou57) 2010-06-03 10:42 ` Brian Drummond @ 2010-06-03 13:49 ` (see below) 2010-06-04 13:49 ` Georg Bauhaus 1 sibling, 1 reply; 95+ messages in thread From: (see below) @ 2010-06-03 13:49 UTC (permalink / raw) On 03/06/2010 04:16, in article op.vdpfdcgoxmjfy8@garhos, "Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote: > Le Thu, 27 May 2010 17:21:57 +0200, (see below) > <yaldnif.w@blueyonder.co.uk> a �crit: >> My experience is that CS/SE students always focus on "coding" at the >> expense >> of problem analysis, program design, project planning, verification, >> validation, documentation, and anything else they find less congenial. > I always though this was not so much with these students. So why do they > choose it if they are not aware of what it requires ? They are aware. That makes no difference. >> Beware: My ex-students are some of the people who >> wrote the software you are using today. ;-) >> > You're teacher too like Stefan ? Was. Now I'm a free man. 8-) -- Bill Findlay <surname><forename> chez blueyonder.co.uk ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-03 13:49 ` (see below) @ 2010-06-04 13:49 ` Georg Bauhaus 2010-06-04 13:53 ` Georg Bauhaus ` (2 more replies) 0 siblings, 3 replies; 95+ messages in thread From: Georg Bauhaus @ 2010-06-04 13:49 UTC (permalink / raw) On 03.06.10 15:49, (see below) wrote: > On 03/06/2010 04:16, in article op.vdpfdcgoxmjfy8@garhos, "Yannick Duch�ne > (Hibou57)" <yannick_duchene@yahoo.fr> wrote: > >> Le Thu, 27 May 2010 17:21:57 +0200, (see below) >> <yaldnif.w@blueyonder.co.uk> a �crit: >>> My experience is that CS/SE students always focus on "coding" at the >>> expense >>> of problem analysis, program design, project planning, verification, >>> validation, documentation, and anything else they find less congenial. >> I always though this was not so much with these students. So why do they >> choose it if they are not aware of what it requires ? > > They are aware. That makes no difference. Coding invariables makes me think of a tricky(?) question: What should a language look like that naturally makes the programmer think before coding, and take his/her time? What would its features and offerings have to be? One inescapable ingredient of any popular PL seems to be magic at the level of syntax, if this is how programmers most visibly see themselves express themselves. Can't force them to wear boring ties. Eiffel's syntax appears to be expanding ... If overloadings of polymorphically clever ASCII punctuation digraphs offer the neccessary magic, I guess this will explain OCaml and its MS adaptation F#, soon to be pushed into the market. Bracket free... Maybe some Cobol style modules headers listing major internal and external parts to be manipulated might help? ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-04 13:49 ` Georg Bauhaus @ 2010-06-04 13:53 ` Georg Bauhaus 2010-06-04 14:24 ` Yannick Duchêne (Hibou57) 2010-06-04 15:29 ` (see below) 2 siblings, 0 replies; 95+ messages in thread From: Georg Bauhaus @ 2010-06-04 13:53 UTC (permalink / raw) On 04.06.10 15:49, Georg Bauhaus wrote: > On 03.06.10 15:49, (see below) wrote: >> On 03/06/2010 04:16, in article op.vdpfdcgoxmjfy8@garhos, "Yannick Duch�ne >> (Hibou57)" <yannick_duchene@yahoo.fr> wrote: >> >>> Le Thu, 27 May 2010 17:21:57 +0200, (see below) >>> <yaldnif.w@blueyonder.co.uk> a �crit: >>>> My experience is that CS/SE students always focus on "coding" at the >>>> expense >>>> of problem analysis, program design, project planning, verification, >>>> validation, documentation, and anything else they find less congenial. >>> I always though this was not so much with these students. So why do they >>> choose it if they are not aware of what it requires ? >> >> They are aware. That makes no difference. > > Coding invariables makes me think of a tricky(?) question: invariably (Must not think of tricky questions while writing...) ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-04 13:49 ` Georg Bauhaus 2010-06-04 13:53 ` Georg Bauhaus @ 2010-06-04 14:24 ` Yannick Duchêne (Hibou57) 2010-06-04 17:34 ` Georg Bauhaus 2010-06-04 15:29 ` (see below) 2 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-06-04 14:24 UTC (permalink / raw) Le Fri, 04 Jun 2010 15:49:49 +0200, Georg Bauhaus <rm.dash-bauhaus@futureapps.de> a écrit: > Coding invariables makes me think of a tricky(?) question: > What should a language look like that naturally makes the programmer > think before coding, and take his/her time? What would its > features and offerings have to be? Undoubtedly, I would think to start with a VDM like (whose theory I know a bit, however never practiced, sorry) I don't mean Ada is not nice for that (it has many things which suggest you to think about the logic and structure of things before to start, and SPARK completes it has it give logic), I just mean this has some additional things, which make it mandatory (based on what I read about it some 15 years ago). Do you agree with that idea ? My advocating: it starts with high level expressions [*], which are not even compilable (don't even think about such a word as “coding” in this context). Then you go down to implementation step by step, and each step has to be proved (the kind of proof it uses is comparable in some way to the ones of SPARK). There is no other road than, first, know what you want (very important), then, know why it can be implemented this/that way (requirement: intuitions, as with any logic/mathematical proof). [*] Please, don't tell me UML do the same, although it may be nice for communication (another area). > One inescapable ingredient of any popular PL seems to be magic at the > level of syntax, if this is how programmers most visibly see themselves > express themselves. Can't force them to wear boring ties. Eiffel's > syntax appears to be expanding ... I did not understood this sentence: “Eiffel's syntax appears to be expanding ...” What you were you to mean ? > Maybe some Cobol style modules headers listing major internal > and external parts to be manipulated might help? Can you give a short example of what it would look like for ones who don't know COBOL ? Are you to complete your list of thoughts about programming languages in the large ? (I remember you talked about it if I'm not wrong) -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-04 14:24 ` Yannick Duchêne (Hibou57) @ 2010-06-04 17:34 ` Georg Bauhaus 0 siblings, 0 replies; 95+ messages in thread From: Georg Bauhaus @ 2010-06-04 17:34 UTC (permalink / raw) On 04.06.10 16:24, Yannick Duchêne (Hibou57) wrote: > Le Fri, 04 Jun 2010 15:49:49 +0200, Georg Bauhaus > <rm.dash-bauhaus@futureapps.de> a écrit: >> Coding invariables makes me think of a tricky(?) question: >> What should a language look like that naturally makes the programmer >> think before coding, and take his/her time? What would its >> features and offerings have to be? > Undoubtedly, I would think to start with a VDM like (whose theory I know > a bit, however never practiced, sorry) > > I don't mean Ada is not nice for that (it has many things which suggest > you to think about the logic and structure of things before to start, > and SPARK completes it has it give logic), I just mean this has some > additional things, which make it mandatory (based on what I read about > it some 15 years ago). > > Do you agree with that idea ? I guess VDM or Z or B means contracts for module interfaces. These work mostly at the level of type construction and associated subprogram profiles. What I have in mind is programmers answering "system design questions" on the one hand versus language support on the other hand. Here is a question: "What typical collection of types/modules would I have to use, and in which way, in order to have a system that performs this or that use case?" Surely, answering this question involves entities whose specific properties are, maybe, programmed in some programming language. But they are not "naturally expressed" in the programming language, there are no "intrinsics" to express system design ("architecture"). You think about module relations. You think about usage patterns. Is there a formalism for such relations that is not some variation of UML? I think that, yes, there is, or might be: I vaguely remember work by David C. Luckham (the name that is associated with the ANNA annotations language) about architecture and a formalism for it. For example, one could start from the observation that novel web based application design forces certain construction principles. These are not directly expressible in any language available for programming in such an environment. (I don't know any such language, that is.) I'm picking Google App Engine as one example of a different computer model: (1) Stop using files for storage. (Google data store, AWS S3 (that's Amazon Web Services), WebDAV, HTML5, or whatever; all without "file pointers", and no streams.) (2) you must process your data not at once but in steps so that Google's quota system and web request processing logic is satisfied. Google App Engine is different, as an operating system. Programming in this environment means - writing request handlers as you "normally" would. But they must do little or else they will be killed - writing request handlers to be added to task queues (task in the non-Ada sense) for background processing, to be called by the GAE's queuing system, and - writing request handlers to be run as cron jobs; these are web requests initiated by the GAE environment at specified times, or else N times per period. Note: all request processing is subject to quota, so you had better design your program following these restrictions (no large chunks). Right now, to establish a "program" in Google App Engine, you use - programming languages Python or Java, - a set of libraries, - configuration scripts, and notably - recommendations and *conventions* layed out in the documentation. It feels like you have to *emulate* the "real language", a language that has words and symbols for the computer model that Google App Engine establishes. But you can only follow the GAE rules. The programming language has no constructs to help you *specifically*. Couldn't there be an expressive formalism that better addresses the issues? > I did not understood this sentence: “Eiffel's syntax appears to be > expanding ...” > What you were you to mean ? It looks like keywords keep being added to Eiffel, for example in the context of iterators. Like Ada's for loop would get syntax to make Has_Element/Element/Next automatic. >> Maybe some Cobol style modules headers listing major internal >> and external parts to be manipulated might help? > Can you give a short example of what it would look like for ones who > don't know COBOL ? My knowledge of Cobol is close to non-existent, but I know that a Cobol program has divisions, Identification Division. ... Environment Division. ... Data Division. ... Procedure Division. ... And there is an "input-output section" in the "Environment Division". This is where you talk about files that your program is going to use. To me, this is a vast improvement over scanning a source tree for possible I/O related fragments. > Are you to complete your list of thoughts about programming languages in > the large ? (I remember you talked about it if I'm not wrong) A complete list? A complete list would be quite an achievement ... ;-) But I am collecting thoughts and, fortunately, I'm not alone. For example, researchers have consistently identified properties of programming language properties that help majorities of programmers (students) get their programs right. Typically they have used some approximation to controlled teaching experiment. Things that don't help: + Overly complicated or strange syntax. + Syntax abstracting away the differences (The expression A(X) has even more meanings in Turing than it has in Ada, wiping out the possibility of understanding what is meant, just by looking at an expression. This finding is at odds with the purpose for which Turing was intended, IIUC!) + Absurdly unhelpful error messages caused by e.g. the "run-away properties" of a language's grammar. (Syntax error at end of file... template spit... Hm. I still have to complain about GNAT's wording, telling me that S : String may assume lower bound of one in expression S(1)...) + Lack of subsetting the language. This means that meaningless compiler messages cannot be avoided when translating a subset; you don't know yet what they mean when you have mistakenly used some advanced language concept. (Turn on Ravenscar and you see "not supported when Ravenscar profile is in effect" or similar for certain constructs. PLT Scheme has teach packs restricting the language similar to Ada profiles.) ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-06-04 13:49 ` Georg Bauhaus 2010-06-04 13:53 ` Georg Bauhaus 2010-06-04 14:24 ` Yannick Duchêne (Hibou57) @ 2010-06-04 15:29 ` (see below) 2 siblings, 0 replies; 95+ messages in thread From: (see below) @ 2010-06-04 15:29 UTC (permalink / raw) On 04/06/2010 14:49, in article 4c09047d$0$6976$9b4e6d93@newsspool4.arcor-online.net, "Georg Bauhaus" <rm.dash-bauhaus@futureapps.de> wrote: > On 03.06.10 15:49, (see below) wrote: >> On 03/06/2010 04:16, in article op.vdpfdcgoxmjfy8@garhos, "Yannick Duch�ne >> (Hibou57)" <yannick_duchene@yahoo.fr> wrote: >> >>> Le Thu, 27 May 2010 17:21:57 +0200, (see below) >>> <yaldnif.w@blueyonder.co.uk> a �crit: >>>> My experience is that CS/SE students always focus on "coding" at the >>>> expense >>>> of problem analysis, program design, project planning, verification, >>>> validation, documentation, and anything else they find less congenial. >>> I always though this was not so much with these students. So why do they >>> choose it if they are not aware of what it requires ? >> >> They are aware. That makes no difference. > > Coding invariables makes me think of a tricky(?) question: > What should a language look like that naturally makes the programmer > think before coding, and take his/her time? I don't think this has anything to do with PL design. It is to do with competence, and a professional attitude. Programmers who possess those qualities work well, even in C. -- Bill Findlay <surname><forename> chez blueyonder.co.uk ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 15:37 ` Dmitry A. Kazakov 2010-05-12 16:06 ` Yannick Duchêne (Hibou57) @ 2010-05-12 18:10 ` stefan-lucks 2010-05-12 17:48 ` Dmitry A. Kazakov 1 sibling, 1 reply; 95+ messages in thread From: stefan-lucks @ 2010-05-12 18:10 UTC (permalink / raw) On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > 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 respect. In C, if I try to compute the factorial of a (natural) number, I'll always get an answer (assuming a decent program, which can be written by a first-year computer science student, and a normal C-compiler). The answer may be right or wrong. If the input is too large, the answer actually is wrong (our first-year student stores the result in an int variable, and 100! is too large). But I still get an answer, even if it is wrong. In Eiffel, I'll either get an answer, or the program will tell that at some point of time when computing, say, the factorial of 100, a certain exception has been raised. (I didn't try out Eiffel, but that is what I would expect.) But if I get an answer, I can be sure it is the right one. That is partial correctness. In SPARK, the examiner (or the simplifier or the proof checker) will tell me that my program is only correct if I specify a certain precondition (e.g., if the input is less than some upper bound). So in SPARK, I can be sure that I'll get the right answer, and SPARK forces me to specify the proper preconditions to get the right answer. Except that even a proper SPARK program might run in an infinite loop ... In any case, there is a huge difference between SPARK and Eiffel, but also between Eiffel and C. > The point is that run-time checks contribute nothing to correctness either > partial or not. Because a partially incorrect program remains partially > incorrect independently on whether you check that or not: Technically, any program of the form {Any Precondition} Statements; if not Postcondition then raise Program_Error; end if; {Postcondition} is partially correct, even if "Statements;" are semantic nonsense (as long as the whole thing compiles at all), regardless of "{Any Precondition}". Perhaps you don't like raising an exception? OK, we can stick with the original approach from Hoare from 1969, who didn't know (or didn't care) about exceptions. The following program is partially correct, regardless of the "Statements;" and "{Any Precondition}": {Any Precondition} Statements; while not Postcondition loop null; end loop; {Postcondition} Actually, the second program could be written in SPARK. It would pass all the static verification performed by the SPARK toolset chain, without leaving any unproven verification conditions. Still, when running the program I can only trust that if I get a result, it satisfies my precondition -- but I can't be sure it satisfies my precondition. More natural -- but not necessarily better -- is the following program: {Any Precondition} while not Postcondition loop Statements; end loop; {Postcondition} Same problem: partial correctness is trivial, regardless of "Statements;". 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! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 18:10 ` stefan-lucks @ 2010-05-12 17:48 ` Dmitry A. Kazakov 2010-05-13 0:37 ` stefan-lucks 0 siblings, 1 reply; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-12 17:48 UTC (permalink / raw) On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks@see-the.signature wrote: > On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > >> 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 respect. > > In C, if I try to compute the factorial of a (natural) number, I'll always > get an answer (assuming a decent program, which can be written by a > first-year computer science student, and a normal C-compiler). > may be right or wrong. If the input is too large, the answer actually is > wrong (our first-year student stores the result in an int variable, and > 100! is too large). But I still get an answer, even if it is wrong. > > In Eiffel, I'll either get an answer, or the program will tell that at > some point of time when computing, say, the factorial of 100, a certain > exception has been raised. (I didn't try out Eiffel, but that is what I > would expect.) But if I get an answer, I can be sure it is the right one. > That is partial correctness. 1. Wrong answer is no more/less incorrect as an exception. Otherwise you have to introduce some scale of correctness, which is called accuracy. A program can yield more or less accurate results staying correct. 2. It is unrelated to error checks. The programmer did not use any. That Eiffel possibly checks for integer overflow and C does not is irrelevant to the issue. >> The point is that run-time checks contribute nothing to correctness either >> partial or not. Because a partially incorrect program remains partially >> incorrect independently on whether you check that or not: > > Technically, any program of the form > > {Any Precondition} > Statements; > if not Postcondition then > raise Program_Error; > end if; > {Postcondition} > > is partially correct, even if "Statements;" are semantic nonsense (as long > as the whole thing compiles at all), regardless of "{Any Precondition}". No. If Statements were irrelevant, you could take this: {Any Precondition} raise Program_Error; {Postcondition} The problem is that Program_Error does not satisfy postcondition. > Perhaps you don't like raising an exception? I don't like any action upon a failed check, if that was a check. To self checks are clearly infeasible. > OK, we can stick with the original approach from Hoare from 1969, who > didn't know (or didn't care) about exceptions. His approach, which I greatly appreciate, is perfectly compatible with exceptions. Exception propagation is a part of the program behavior to be checked as anything else. E.g. pre : x = 1 if x = 1 then raise Foo; end if; post : Foo propagating This program were be incorrect if it would not raise Foo. > The following program is > partially correct, regardless of the "Statements;" and "{Any > Precondition}": > > {Any Precondition} > Statements; > while not Postcondition loop > null; > end loop; > {Postcondition} Hmm, I would consider it totally incorrect => not partially incorrect, because in no state it satisfies the postcondition. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 17:48 ` Dmitry A. Kazakov @ 2010-05-13 0:37 ` stefan-lucks 2010-05-13 9:09 ` Dmitry A. Kazakov 0 siblings, 1 reply; 95+ messages in thread From: stefan-lucks @ 2010-05-13 0:37 UTC (permalink / raw) On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks@see-the.signature wrote: > > > In Eiffel, I'll either get an answer, or the program will tell that at > > some point of time when computing, say, the factorial of 100, a certain > > exception has been raised. (I didn't try out Eiffel, but that is what I > > would expect.) But if I get an answer, I can be sure it is the right one. > > That is partial correctness. > > 1. Wrong answer is no more/less incorrect as an exception. We clearly disagree on this point. Consider being new in a town, and asking how to go from, say, the railway station to the market place. If we ask a guy who appears to be a local person in our eyes, but is actually as foreing as we are, most people would prefer an exception "sorry, I don't know the way" over the answer of being directed into the wrong direction. If you think, the "sorry" is as bad as the wrong direction, that is your problem, which I am not interested in discussing any further. Yes, there are some applications where the exception is just as bad as the wrong answer. One such example could be the autopilot of a plane. The plane may crash because the autopilot stops working, or because the autopilot acts on wrong results. Crash is crash. But not all applications have that severe requirments. In fact, event he autopilot may benefit from checks -- if these are performed when the plane is still on the ground, and if any failed test prevents the plane from starting. > 2. It is unrelated to error checks. The programmer did not use any. That > Eiffel possibly checks for integer overflow and C does not is irrelevant to > the issue. The exception may just as well be raised when checking the postcondition. > {Any Precondition} > raise Program_Error; > {Postcondition} Yes, that program is partially correct. Well, Hoare did originally not bother with exceptions, but the following program is partially correct even in the old we-do-not-know-about-exceptions sense: {Any Precondition} while false loop null; end loop; {Postcondition} > The problem is that Program_Error does not satisfy postcondition. > His approach, which I greatly appreciate, is perfectly compatible with > exceptions. Exception propagation is a part of the program behavior to be > checked as anything else. E.g. > > pre : x = 1 > if x = 1 then > raise Foo; > end if; > post : Foo propagating > > This program were be incorrect if it would not raise Foo. Now I see what you mean. You are asking for contracts which include exception propagation. Yes, that would be nice to have. Then you should like Eiffel, because this is what Eiffel actually does. In Eiffel, the formal postcondition require P; is a shortcut notation for the logical Postcondition: P or else (Postcondition_Violation propagating); (whatever the name of the exception is), which is the real postcondition of an Eiffel program. If Eiffel checks P at the end of the program, and raises that exception when the check fails, then Eiffel-programs are always correct! You don't even need to perform any static analysis to ensure their correctness. (But you must not turn of the checks!) Of course the catch is that you would rather want to specify postconditions which exclude exception propagation. I.e., you would need formal postconditions *without* the "or else propagate something" part. In Eiffel, there is no way to enforce such postconditions. And how should that be possible, without static analysis? Perhaps, the difference between SPARK and Eiffel DbC can be summarised as follows: -> Eiffel is a very expressive programming language, while SPARK is less expressive. -> The language for contracts in SPARK is more expressive than the language for contracts in Eiffel. That doesn't mean that the contracts you can express in Eiffel are invalid, however. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-13 0:37 ` stefan-lucks @ 2010-05-13 9:09 ` Dmitry A. Kazakov 0 siblings, 0 replies; 95+ messages in thread From: Dmitry A. Kazakov @ 2010-05-13 9:09 UTC (permalink / raw) On Thu, 13 May 2010 02:37:37 +0200, stefan-lucks@see-the.signature wrote: > On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > >> On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks@see-the.signature wrote: >> >>> In Eiffel, I'll either get an answer, or the program will tell that at >>> some point of time when computing, say, the factorial of 100, a certain >>> exception has been raised. (I didn't try out Eiffel, but that is what I >>> would expect.) But if I get an answer, I can be sure it is the right one. >>> That is partial correctness. >> >> 1. Wrong answer is no more/less incorrect as an exception. > > We clearly disagree on this point. > > Consider being new in a town, and asking how to go from, say, the railway > station to the market place. If we ask a guy who appears to be a local > person in our eyes, but is actually as foreing as we are, most people > would prefer an exception "sorry, I don't know the way" over the answer of > being directed into the wrong direction. If you think, the "sorry" is as > bad as the wrong direction, that is your problem, which I am not > interested in discussing any further. Consider another example. Let you have a word processor, which also calculates frequencies of some words. After typing dozen pages of the document, you remove a word (the last instance, occasionally), and the processor crashes on zero divide trying to calculate its new frequency. I bet you would prefer a rubbish frequency displayed. The bottom line, the effect of an error is undefined. You cannot define any reasonable action upon, UNLESS further information were available. Which is equivalent to *specification* of a behavior. Once the behavior is defined, it is no more an error, e.g. the frequency of an unused word is displayed as an empty string. It is a mere requirement. If you don't know the answer, say "I don't know", do not shoot. >> 2. It is unrelated to error checks. The programmer did not use any. That >> Eiffel possibly checks for integer overflow and C does not is irrelevant to >> the issue. > > The exception may just as well be raised when checking the postcondition. or from an if-statement placed by the programmer. >> {Any Precondition} >> raise Program_Error; >> {Postcondition} > > Yes, that program is partially correct. I wouldn't consider it as such. > Well, Hoare did originally not bother with exceptions, BTW Hoare, wasn't it actually Edsger Dijkstra? >> The problem is that Program_Error does not satisfy postcondition. > >> His approach, which I greatly appreciate, is perfectly compatible with >> exceptions. Exception propagation is a part of the program behavior to be >> checked as anything else. E.g. >> >> pre : x = 1 >> if x = 1 then >> raise Foo; >> end if; >> post : Foo propagating >> >> This program were be incorrect if it would not raise Foo. > > Now I see what you mean. You are asking for contracts which include > exception propagation. Yes, that would be nice to have. How could it be otherwise? > Then you should like Eiffel, because this is what Eiffel actually does. In > Eiffel, the formal postcondition > > require P; > > is a shortcut notation for the logical > > Postcondition: P or else (Postcondition_Violation propagating); > > (whatever the name of the exception is), which is the real postcondition > of an Eiffel program. If Eiffel checks P at the end of the program, and > raises that exception when the check fails, then > > Eiffel-programs are always correct! Yes. Therefore a lazy programmer could write raise Postcondition_Violation; and claim his salary. > You don't even need to perform any static analysis to ensure their > correctness. (But you must not turn of the checks!) Nice language, the program semantics depends on the compiler options. (We have this in some places in Ada too, unfortunately) > Of course the catch is that you would rather want to specify > postconditions which exclude exception propagation. Yep. > -> Eiffel is a very expressive programming language, > while SPARK is less expressive. > > -> The language for contracts in SPARK is more expressive > than the language for contracts in Eiffel. OK > That doesn't mean that the contracts you can express in Eiffel are > invalid, however. With the addition you made they are not. Once you remove Postcondition_Violation (which can be done by a compiler switch), they become invalid. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-12 8:41 ` stefan-lucks 2010-05-12 14:52 ` Yannick Duchêne (Hibou57) 2010-05-12 15:37 ` Dmitry A. Kazakov @ 2010-05-13 0:33 ` Yannick Duchêne (Hibou57) 2 siblings, 0 replies; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-13 0:33 UTC (permalink / raw) Le Wed, 12 May 2010 10:41:03 +0200, <stefan-lucks@see-the.signature> a écrit: > 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. > > [...] > > (**) 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? At the end of [Praxis SPARK 95 4.5] you may read the following : > It is also guaranteed that code is “reducible”, i.e. that > every loop has a single entry point, simplifying the > generation of verification conditions from loop invariants. So there are some proofs also made on loops at least (still need to learn more). -- pragma Asset ? Is that true ? Waaww... great ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT Pro license (was: GNAT packages in Linux distributions 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) ` (2 preceding siblings ...) 2010-05-10 8:02 ` Dmitry A. Kazakov @ 2010-05-10 14:15 ` Peter Hermann 3 siblings, 0 replies; 95+ messages in thread From: Peter Hermann @ 2010-05-10 14:15 UTC (permalink / raw) Yannick Duch??ne (Hibou57) <yannick_duchene@yahoo.fr> wrote: > P.P.S. I wonder why, being an owner of a GNAT Pro license, you need the > GPL version ? You will get just less with the GPL version. if you are teacher you need the free version too in order to adapt to the level of your students or readers even if you had the GNATpro version bought by your company. another reason may be retirement: you cant afford the license prices privately. www.ihr.uni-stuttgart.de/forschung/ada/resources_on_ada/ ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-09 17:40 GNAT packages in Linux distributions Dmitry A. Kazakov 2010-05-09 18:16 ` Ludovic Brenta @ 2010-05-10 1:40 ` Björn Persson 2010-05-10 2:04 ` Yannick Duchêne (Hibou57) 1 sibling, 1 reply; 95+ messages in thread From: Björn Persson @ 2010-05-10 1:40 UTC (permalink / raw) Dmitry A. Kazakov wrote: > For more than a year I has been using either GNAT Pro or GNAT GPL. > Recently I installed Fedora and Debian GNAT distributions and discovered > that basically all two years old bugs known to me are still present. Some > of these bugs were fixed in GNAT GPL 2009, others in GNAT Pro 6.3. > > So my question is: is there any information or summary on the Web about > how Linux distributions are related to AdaCore releases? Or maybe somebody > knowledgeable could create and maintain this as a wiki etc. I don't think Fedora has a written policy or some such for how compilers are packaged, but as far as I know they take a GCC release from the FSF, add a few patches related to C, C++ and Java, and compile it with all languages enabled. I get the impression that GNAT is in Fedora only because it's part of GCC. That means that before a bugfix from AdaCore ends up in a Fedora release, it must first be part of a merge from AdaCore to the FSF's code tree. I've heard that they merge only to the trunk during development stage 1. Some time later the FSF makes a release branch from the trunk and refines the branch into a release. Then the Fedora packagers upgrade the GCC package in Rawhide, the development repository, to the new release, which again is done only in an early development stage as it can be a fairly disruptive change. Later Rawhide is branched, and the branch goes through months of testing and bug-fixing and eventually becomes the next Fedora release. Naturally this process takes a long time. Fedora 13 Beta has GCC 4.4.3. I think we'll probably see GCC 4.5 in Fedora 14, but at the moment Rawhide is at 4.4.4. -- Bj�rn Persson PGP key A88682FD ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 1:40 ` Björn Persson @ 2010-05-10 2:04 ` Yannick Duchêne (Hibou57) 2010-05-10 7:01 ` Ludovic Brenta 0 siblings, 1 reply; 95+ messages in thread From: Yannick Duchêne (Hibou57) @ 2010-05-10 2:04 UTC (permalink / raw) Thanks for these detailed explanations, > That means that before a bugfix from AdaCore ends up in a Fedora > release, it > must first be part of a merge from AdaCore to the FSF's code tree. I've > heard that they merge only to the trunk during development stage 1. What does “Stage 1” stands for exactly ? What happens and what's done on this Stage 1 ? -- No-no, this isn't an oops ...or I hope (TM) - Don't blame me... I'm just not lucky ^ permalink raw reply [flat|nested] 95+ messages in thread
* Re: GNAT packages in Linux distributions 2010-05-10 2:04 ` Yannick Duchêne (Hibou57) @ 2010-05-10 7:01 ` Ludovic Brenta 0 siblings, 0 replies; 95+ messages in thread From: Ludovic Brenta @ 2010-05-10 7:01 UTC (permalink / raw) Yannick Duchêne writes on comp.lang.ada: > Thanks for these detailed explanations, > >> That means that before a bugfix from AdaCore ends up in a Fedora >> release, it >> must first be part of a merge from AdaCore to the FSF's code tree. I've >> heard that they merge only to the trunk during development stage 1. > What does “Stage 1” stands for exactly ? What happens and what's done > on this Stage 1 ? See http://gcc.gnu.org/develop.html The delay between the end of Stage 1 and the official release of GCC was typically between 8 and 10 months up to GCC 4.3; for GCC 4.4 and 4.5 the developers decided to skip Stage 2 entirely and this reduced the delay to 5 months in GCC 4.4 and 6 months in GCC 4.5. This delay accounts for part of the delay between a bug fix in GNAT Pro and the corresponding bug fix in the next GCC release. However, some bug fixes are backported into the previous release and into Debian, so they become available as early as practical. -- Ludovic Brenta. ^ permalink raw reply [flat|nested] 95+ messages in thread
end of thread, other threads:[~2010-06-04 17:34 UTC | newest] Thread overview: 95+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2010-05-09 17:40 GNAT packages in Linux distributions Dmitry A. Kazakov 2010-05-09 18:16 ` Ludovic Brenta 2010-05-09 19:36 ` Dmitry A. Kazakov 2010-05-09 21:26 ` Ludovic Brenta 2010-05-09 21:34 ` Yannick Duchêne (Hibou57) 2010-05-10 1:20 ` Ludovic Brenta 2010-05-10 1:26 ` Ludovic Brenta 2010-05-25 20:40 ` Yannick Duchêne (Hibou57) 2010-05-10 9:41 ` Stephen Leake 2010-05-10 9:46 ` Ludovic Brenta 2010-05-10 14:29 ` sjw 2010-05-11 7:51 ` Ludovic Brenta 2010-05-11 9:33 ` sjw 2010-05-10 18:47 ` Yannick Duchêne (Hibou57) 2010-05-09 21:28 ` Yannick Duchêne (Hibou57) 2010-05-09 21:30 ` Yannick Duchêne (Hibou57) 2010-05-09 22:44 ` Simon Wright 2010-05-10 7:54 ` Dmitry A. Kazakov 2010-05-10 8:02 ` Dmitry A. Kazakov 2010-05-10 18:45 ` Yannick Duchêne (Hibou57) 2010-05-10 21:00 ` Ludovic Brenta 2010-05-10 22:17 ` Yannick Duchêne (Hibou57) 2010-05-11 6:56 ` Ludovic Brenta 2010-05-11 7:39 ` Dmitry A. Kazakov 2010-05-11 8:06 ` Yannick Duchêne (Hibou57) 2010-05-11 15:46 ` Pascal Obry 2010-05-11 16:05 ` Yannick Duchêne (Hibou57) 2010-05-11 16:09 ` Pascal Obry 2010-05-11 16:09 ` Pascal Obry 2010-05-11 17:08 ` stefan-lucks 2010-05-11 16:39 ` Yannick Duchêne (Hibou57) 2010-05-11 19:45 ` Yannick Duchêne (Hibou57) 2010-05-11 23:44 ` Yannick Duchêne (Hibou57) 2010-05-12 12:12 ` Mark Lorenzen 2010-05-12 14:55 ` Yannick Duchêne (Hibou57) 2010-05-11 17:35 ` Pascal Obry 2010-05-11 18:06 ` Yannick Duchêne (Hibou57) 2010-05-11 16:23 ` Yannick Duchêne (Hibou57) 2010-05-11 16:41 ` J-P. Rosen 2010-05-11 16:45 ` Dmitry A. Kazakov 2010-05-11 19:21 ` Yannick Duchêne (Hibou57) 2010-05-12 8:41 ` stefan-lucks 2010-05-12 14:52 ` Yannick Duchêne (Hibou57) 2010-05-12 15:59 ` Phil Thornley 2010-05-12 16:49 ` Yannick Duchêne (Hibou57) 2010-05-13 8:05 ` Phil Thornley 2010-05-12 15:37 ` Dmitry A. Kazakov 2010-05-12 16:06 ` Yannick Duchêne (Hibou57) 2010-05-12 17:24 ` Dmitry A. Kazakov 2010-05-12 18:09 ` Georg Bauhaus 2010-05-12 18:33 ` Dmitry A. Kazakov 2010-05-12 18:53 ` Georg Bauhaus 2010-05-12 21:57 ` Dmitry A. Kazakov 2010-05-13 2:03 ` Georg Bauhaus 2010-05-13 8:39 ` Dmitry A. Kazakov 2010-05-14 23:45 ` Georg Bauhaus 2010-05-15 9:30 ` Dmitry A. Kazakov 2010-05-15 18:39 ` Georg Bauhaus 2010-05-15 20:33 ` Dmitry A. Kazakov 2010-05-15 0:17 ` Robert A Duff 2010-05-15 9:40 ` Dmitry A. Kazakov 2010-05-12 18:15 ` Georg Bauhaus 2010-05-25 20:45 ` Yannick Duchêne (Hibou57) 2010-05-26 7:55 ` Dmitry A. Kazakov 2010-05-26 8:38 ` stefan-lucks 2010-05-26 8:01 ` Yannick Duchêne (Hibou57) 2010-05-26 11:25 ` Yannick Duchêne (Hibou57) 2010-05-26 13:02 ` stefan-lucks 2010-05-26 12:22 ` Yannick Duchêne (Hibou57) 2010-05-27 12:47 ` stefan-lucks 2010-05-27 12:26 ` Yannick Duchêne (Hibou57) 2010-05-26 13:06 ` (see below) 2010-05-27 12:41 ` stefan-lucks 2010-05-27 12:29 ` Yannick Duchêne (Hibou57) 2010-05-27 15:21 ` (see below) 2010-06-03 3:16 ` Yannick Duchêne (Hibou57) 2010-06-03 10:42 ` Brian Drummond 2010-06-03 21:14 ` (see below) 2010-06-03 22:00 ` Britt Snodgrass 2010-06-03 22:29 ` (see below) 2010-06-03 13:49 ` (see below) 2010-06-04 13:49 ` Georg Bauhaus 2010-06-04 13:53 ` Georg Bauhaus 2010-06-04 14:24 ` Yannick Duchêne (Hibou57) 2010-06-04 17:34 ` Georg Bauhaus 2010-06-04 15:29 ` (see below) 2010-05-12 18:10 ` stefan-lucks 2010-05-12 17:48 ` Dmitry A. Kazakov 2010-05-13 0:37 ` stefan-lucks 2010-05-13 9:09 ` Dmitry A. Kazakov 2010-05-13 0:33 ` Yannick Duchêne (Hibou57) 2010-05-10 14:15 ` GNAT Pro license (was: " Peter Hermann 2010-05-10 1:40 ` Björn Persson 2010-05-10 2:04 ` Yannick Duchêne (Hibou57) 2010-05-10 7:01 ` Ludovic Brenta
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox