From: stefan-lucks on
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! ------
From: Dmitry A. Kazakov on
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(a)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
From: Yannick Duchêne (Hibou57) on
Le Wed, 26 May 2010 10:38:20 +0200, <stefan-lucks(a)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.
From: Yannick Duchêne (Hibou57) on
Le Wed, 26 May 2010 10:38:20 +0200, <stefan-lucks(a)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.
From: stefan-lucks on
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! ------