From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Re: GNAT packages in Linux distributions
Date: Wed, 12 May 2010 18:06:16 +0200
Date: 2010-05-12T18:06:16+02:00 [thread overview]
Message-ID: <op.vclocqp9ule2fv@garhos> (raw)
In-Reply-To: 1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net
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
next prev parent reply other threads:[~2010-05-12 16:06 UTC|newest]
Thread overview: 95+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-05-09 17:40 GNAT packages in Linux distributions Dmitry A. Kazakov
2010-05-09 18:16 ` Ludovic Brenta
2010-05-09 19:36 ` Dmitry A. Kazakov
2010-05-09 21:26 ` Ludovic Brenta
2010-05-09 21:34 ` Yannick Duchêne (Hibou57)
2010-05-10 1:20 ` Ludovic Brenta
2010-05-10 1:26 ` Ludovic Brenta
2010-05-25 20:40 ` Yannick Duchêne (Hibou57)
2010-05-10 9:41 ` Stephen Leake
2010-05-10 9:46 ` Ludovic Brenta
2010-05-10 14:29 ` sjw
2010-05-11 7:51 ` Ludovic Brenta
2010-05-11 9:33 ` sjw
2010-05-10 18:47 ` Yannick Duchêne (Hibou57)
2010-05-09 21:28 ` Yannick Duchêne (Hibou57)
2010-05-09 21:30 ` Yannick Duchêne (Hibou57)
2010-05-09 22:44 ` Simon Wright
2010-05-10 7:54 ` Dmitry A. Kazakov
2010-05-10 8:02 ` Dmitry A. Kazakov
2010-05-10 18:45 ` Yannick Duchêne (Hibou57)
2010-05-10 21:00 ` Ludovic Brenta
2010-05-10 22:17 ` Yannick Duchêne (Hibou57)
2010-05-11 6:56 ` Ludovic Brenta
2010-05-11 7:39 ` Dmitry A. Kazakov
2010-05-11 8:06 ` Yannick Duchêne (Hibou57)
2010-05-11 15:46 ` Pascal Obry
2010-05-11 16:05 ` Yannick Duchêne (Hibou57)
2010-05-11 16:09 ` Pascal Obry
2010-05-11 16:09 ` Pascal Obry
2010-05-11 17:08 ` stefan-lucks
2010-05-11 16:39 ` Yannick Duchêne (Hibou57)
2010-05-11 19:45 ` Yannick Duchêne (Hibou57)
2010-05-11 23:44 ` Yannick Duchêne (Hibou57)
2010-05-12 12:12 ` Mark Lorenzen
2010-05-12 14:55 ` Yannick Duchêne (Hibou57)
2010-05-11 17:35 ` Pascal Obry
2010-05-11 18:06 ` Yannick Duchêne (Hibou57)
2010-05-11 16:23 ` Yannick Duchêne (Hibou57)
2010-05-11 16:41 ` J-P. Rosen
2010-05-11 16:45 ` Dmitry A. Kazakov
2010-05-11 19:21 ` Yannick Duchêne (Hibou57)
2010-05-12 8:41 ` stefan-lucks
2010-05-12 14:52 ` Yannick Duchêne (Hibou57)
2010-05-12 15:59 ` Phil Thornley
2010-05-12 16:49 ` Yannick Duchêne (Hibou57)
2010-05-13 8:05 ` Phil Thornley
2010-05-12 15:37 ` Dmitry A. Kazakov
2010-05-12 16:06 ` Yannick Duchêne (Hibou57) [this message]
2010-05-12 17:24 ` Dmitry A. Kazakov
2010-05-12 18:09 ` Georg Bauhaus
2010-05-12 18:33 ` Dmitry A. Kazakov
2010-05-12 18:53 ` Georg Bauhaus
2010-05-12 21:57 ` Dmitry A. Kazakov
2010-05-13 2:03 ` Georg Bauhaus
2010-05-13 8:39 ` Dmitry A. Kazakov
2010-05-14 23:45 ` Georg Bauhaus
2010-05-15 9:30 ` Dmitry A. Kazakov
2010-05-15 18:39 ` Georg Bauhaus
2010-05-15 20:33 ` Dmitry A. Kazakov
2010-05-15 0:17 ` Robert A Duff
2010-05-15 9:40 ` Dmitry A. Kazakov
2010-05-12 18:15 ` Georg Bauhaus
2010-05-25 20:45 ` Yannick Duchêne (Hibou57)
2010-05-26 7:55 ` Dmitry A. Kazakov
2010-05-26 8:38 ` stefan-lucks
2010-05-26 8:01 ` Yannick Duchêne (Hibou57)
2010-05-26 11:25 ` Yannick Duchêne (Hibou57)
2010-05-26 13:02 ` stefan-lucks
2010-05-26 12:22 ` Yannick Duchêne (Hibou57)
2010-05-27 12:47 ` stefan-lucks
2010-05-27 12:26 ` Yannick Duchêne (Hibou57)
2010-05-26 13:06 ` (see below)
2010-05-27 12:41 ` stefan-lucks
2010-05-27 12:29 ` Yannick Duchêne (Hibou57)
2010-05-27 15:21 ` (see below)
2010-06-03 3:16 ` Yannick Duchêne (Hibou57)
2010-06-03 10:42 ` Brian Drummond
2010-06-03 21:14 ` (see below)
2010-06-03 22:00 ` Britt Snodgrass
2010-06-03 22:29 ` (see below)
2010-06-03 13:49 ` (see below)
2010-06-04 13:49 ` Georg Bauhaus
2010-06-04 13:53 ` Georg Bauhaus
2010-06-04 14:24 ` Yannick Duchêne (Hibou57)
2010-06-04 17:34 ` Georg Bauhaus
2010-06-04 15:29 ` (see below)
2010-05-12 18:10 ` stefan-lucks
2010-05-12 17:48 ` Dmitry A. Kazakov
2010-05-13 0:37 ` stefan-lucks
2010-05-13 9:09 ` Dmitry A. Kazakov
2010-05-13 0:33 ` Yannick Duchêne (Hibou57)
2010-05-10 14:15 ` GNAT Pro license (was: " Peter Hermann
2010-05-10 1:40 ` Björn Persson
2010-05-10 2:04 ` Yannick Duchêne (Hibou57)
2010-05-10 7:01 ` Ludovic Brenta
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox