comp.lang.ada
 help / color / mirror / Atom feed
From: "G.B." <bauhaus@futureapps.invalid>
Subject: Re: How to get nice with GNAT?
Date: Tue, 25 Nov 2014 20:18:21 +0100
Date: 2014-11-25T20:18:21+01:00	[thread overview]
Message-ID: <m52kld$s8g$1@dont-email.me> (raw)
In-Reply-To: <8f203a9a-6c7c-4614-bc7d-efa65bf10776@googlegroups.com>

On 25.11.14 16:07, ake.ragnar.dahlgren@gmail.com wrote:
> Of course I always listen seriously to Jeff Carter but it's not obvious to me that doing "C in Ada" is bad. If I remember correctly Google employees are recommended to avoid using exceptions when doing C++. The designers of Google Go has gone great lengths to avoid the exception concept as much as possible. In addition SPARK forbids usage of exceptions.

Tucker Taft, designer of both Ada 95 and ParaSail has not
put Ada's exceptions in his ParaSail language(*). The latter
language does presume a lot of checking at compile time, though,
of logical expressions etc.; all of this is almost entirely absent
from C programs.

That's not without consequences for a fair comparison.

Some static analyzers re-interpret the C language by adding
rules and information that is not present in either C programs
or in the C language. The interpretation may likely be what
the programmers would have intended, but still inference cannot
magically add all of the same logical information to a C program
that would be present in a ParaSail program. Moreover, a program's
meaning then begins to essentially depend on the QoI of a compiler,
not on the language or on your own expressions as a program's author.

As these and previous efforts both at language design and
at compiler technology will influence AdaCore, it seems likely
that Ada 2012's contracts can both reduce the need for checks
at run-time and add assurance based on real expressions,
while also improving diagnostic messages if provers look at
the assertions, the calls, and the implementations.

There are the beginnings specific mentions of exception
identifiers in post-conditions, IIUC.

    Post => that_will_be_true(...) or else raise  ...;

ParaSail...
"eliminates run-time exception handling -- strong compile-time
  checking of preconditions and support for parallel event-handling
  provides a safer alternative;"

__
(*)https://forge.open-do.org/plugins/moinmoin/parasail/


  parent reply	other threads:[~2014-11-25 19:18 UTC|newest]

Thread overview: 59+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2014-11-21 11:41 How to get nice with GNAT? Natasha Kerensikova
2014-11-21 12:42 ` Björn Lundin
2014-11-21 22:55 ` Randy Brukardt
2014-11-21 23:13   ` Björn Lundin
2014-11-22  9:45   ` How to get nice traceback " Natasha Kerensikova
2014-11-22  9:57     ` Dmitry A. Kazakov
2014-11-24 22:35     ` Randy Brukardt
2014-11-22 10:11 ` How to get nice " gautier_niouzes
2014-11-22 10:40   ` Natasha Kerensikova
2014-11-22 22:44 ` brbarkstrom
2014-11-22 23:24   ` Jeffrey Carter
2014-11-23 18:06   ` Björn Lundin
2014-11-23 16:13 ` brbarkstrom
2014-11-23 16:18   ` J-P. Rosen
2014-11-23 17:02   ` Jeffrey Carter
2014-11-23 17:41 ` brbarkstrom
2014-11-23 19:22   ` Simon Wright
2014-11-23 20:49   ` Jeffrey Carter
2014-11-24  3:05     ` brbarkstrom
2014-11-24  6:25       ` Jeffrey Carter
2014-11-24 14:39         ` brbarkstrom
2014-11-24 17:42       ` Dennis Lee Bieber
2014-11-25 13:45         ` brbarkstrom
2014-11-25 15:07           ` ake.ragnar.dahlgren
2014-11-25 15:51             ` brbarkstrom
2014-11-25 16:52             ` Jeffrey Carter
2014-11-25 19:18             ` G.B. [this message]
2014-11-25 20:47               ` brbarkstrom
2014-11-25 22:12             ` Randy Brukardt
2014-11-25 23:30               ` Simon Wright
2014-11-26  1:25                 ` G.B.
2014-11-26  7:35                   ` Simon Wright
2014-11-26 11:55                     ` Georg Bauhaus
2014-11-26 13:06                       ` Dmitry A. Kazakov
2014-11-26 13:36                         ` brbarkstrom
2014-11-26 21:27                         ` Randy Brukardt
2014-11-26 22:38                           ` brbarkstrom
2014-11-27  9:01                             ` Dmitry A. Kazakov
2014-11-27 13:53                               ` brbarkstrom
2014-11-27 17:19                                 ` Dmitry A. Kazakov
2014-12-01 22:25                                   ` Randy Brukardt
2014-12-02  8:42                                     ` Dmitry A. Kazakov
2014-12-03 21:41                                       ` Randy Brukardt
2014-12-06 12:02                                         ` Dmitry A. Kazakov
2014-12-08 22:45                                           ` Randy Brukardt
2014-12-09  8:51                                             ` Dmitry A. Kazakov
2014-12-09 23:14                                               ` Brad Moore
2014-12-09 17:59                                                 ` Dmitry A. Kazakov
2014-11-27  8:52                           ` Dmitry A. Kazakov
2014-11-26  6:18                 ` J-P. Rosen
2014-11-26  7:37                   ` Simon Wright
2014-11-26  8:41               ` Dmitry A. Kazakov
2014-11-25 18:33           ` Dennis Lee Bieber
2014-11-26  1:27             ` Dennis Lee Bieber
2014-11-26  3:29               ` brbarkstrom
2014-11-23 18:55 ` brbarkstrom
2014-11-23 19:30 ` brbarkstrom
2014-11-23 22:38   ` Simon Wright
2014-11-24  2:47     ` brbarkstrom
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox