GNAT packages in Linux distributions

GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[Stephen Leake]

"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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[sjw]

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).

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[sjw]

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 ...

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

> 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

Re: GNAT packages in Linux distributions

[Simon Wright]

"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".

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Pascal Obry]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Pascal Obry]

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

Re: GNAT packages in Linux distributions

[Pascal Obry]

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

Re: GNAT packages in Linux distributions

[stefan-lucks]

[-- 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!  ------

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Mark Lorenzen]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Pascal Obry]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[J-P. Rosen]

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

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[stefan-lucks]

[-- 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!  ------

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Phil Thornley]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Phil Thornley]

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

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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 ...; ?

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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?

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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?

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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).

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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.

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Robert A Duff]

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

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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.

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[stefan-lucks]

[-- 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!  ------

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[stefan-lucks]

[-- 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!  ------

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[stefan-lucks]

[-- 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!  ------

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[(see below)]

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

Re: GNAT packages in Linux distributions

[stefan-lucks]

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!  ------

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[(see below)]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[Brian Drummond]

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

Re: GNAT packages in Linux distributions

[(see below)]

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

Re: GNAT packages in Linux distributions

[Britt Snodgrass]

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.

Re: GNAT packages in Linux distributions

[(see below)]

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

Re: GNAT packages in Linux distributions

[(see below)]

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

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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?

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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...)

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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.

Re: GNAT packages in Linux distributions

[Georg Bauhaus]

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.)

Re: GNAT packages in Linux distributions

[(see below)]

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

Re: GNAT packages in Linux distributions

[stefan-lucks]

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!  ------

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[stefan-lucks]

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!  ------

Re: GNAT packages in Linux distributions

[Dmitry A. Kazakov]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT Pro license (was: GNAT packages in Linux distributions

[Peter Hermann]

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/

Re: GNAT packages in Linux distributions

[Björn Persson]

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

Re: GNAT packages in Linux distributions

[Yannick Duchêne (Hibou57)]

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

Re: GNAT packages in Linux distributions

[Ludovic Brenta]

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.