comp.lang.ada
 help / color / mirror / Atom feed
From: Shark8 <onewingedshark@gmail.com>
Cc: mailbox@dmitry-kazakov.de
Subject: Re: about the new Ada 2012 pre/post conditions
Date: Fri, 29 Jun 2012 14:03:27 -0700 (PDT)
Date: 2012-06-29T14:03:27-07:00	[thread overview]
Message-ID: <ec53fb35-8af6-4d30-9353-f8854feea4cf@googlegroups.com> (raw)
In-Reply-To: <z27igg6796oj$.oefrs9mmhzok$.dlg@40tude.net>


> > What do pre/post implement, if so, in your view?
> 
>    if Pre(...) then
>       <body>
>       if Post(...) then
>          null;
>       else
>          raise Constraint_Error;
>       end if;
>    else
>       raise Constraint_Error;
>    end if;

Ok, but this is just what preconditions [and post] are supposed to do.

After all, we had a way to specify some preconditions before (in Ada 2005):
Type Some_Type is ...;
Type Access_Some is Access Some_Type;
Subtype NN_Access_Some is Not Null Access_Some;

Procedure Default_Handler( Object : NN_Access_Some );

defines a a function [spec] in which the body may assume that Object is not null, as if it is it will raise Constraint_Error, thereby allowing us to get rid of the checking logic within the function.

How does pulling that out into the Pre clause in Ada 2012 change things? Also, is not the general concept now generalizable? (IE so that these assumptions may be safely made.)

I'm really confused on why you seem to think the Pre- and Post-conditions are bad things. That you can compile something that *could* violate them is irrelevant, you could do the same with the given default_handler procedure, especially if you were pulling it from user-input. It has a well defined behavior for the error of trying to pass null in, and moreover you can catch-and-correct it if it is correctable.

Post seems a bit less useful than Pre, but maybe that's because I'm being unimaginative today.



  parent reply	other threads:[~2012-06-29 21:10 UTC|newest]

Thread overview: 125+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi
2012-06-20 14:02 ` Georg Bauhaus
2012-06-20 14:13 ` Dmitry A. Kazakov
2012-06-20 14:24   ` Nasser M. Abbasi
2012-06-20 14:37     ` Dmitry A. Kazakov
2012-06-20 17:02       ` Georg Bauhaus
2012-06-20 18:28         ` Dmitry A. Kazakov
2012-06-21 20:32       ` Randy Brukardt
2012-06-22  7:23         ` Dmitry A. Kazakov
2012-06-22 11:54           ` Georg Bauhaus
2012-06-22 12:39             ` Georg Bauhaus
2012-06-22 12:43             ` Dmitry A. Kazakov
2012-06-22 14:30               ` Georg Bauhaus
2012-06-22 14:36                 ` Georg Bauhaus
2012-06-22 15:05                 ` Dmitry A. Kazakov
2012-06-22 15:52                   ` Georg Bauhaus
2012-06-22 16:35                     ` Dmitry A. Kazakov
2012-06-22 16:53                       ` Georg Bauhaus
2012-06-22 16:45                   ` Georg Bauhaus
2012-06-22 17:24                     ` Dmitry A. Kazakov
2012-06-22 19:41           ` Randy Brukardt
2012-06-22 23:08             ` Dmitry A. Kazakov
2012-06-23 10:46               ` Georg Bauhaus
2012-06-23 11:01                 ` Dmitry A. Kazakov
2012-06-23 17:46                   ` AdaMagica
2012-06-23 19:23                     ` Dmitry A. Kazakov
2012-06-24 14:59                   ` Georg Bauhaus
2012-06-24 16:06                     ` Dmitry A. Kazakov
2012-06-24 19:51                       ` Georg Bauhaus
2012-06-25  7:48                         ` Dmitry A. Kazakov
2012-06-25 10:10                           ` Georg Bauhaus
2012-06-25  8:08                         ` Dmitry A. Kazakov
2012-06-25 10:17                           ` Georg Bauhaus
2012-06-25 11:54                             ` Dmitry A. Kazakov
2012-06-25 12:39                               ` Georg Bauhaus
2012-06-25 12:51                                 ` Georg Bauhaus
2012-06-25 13:19                                 ` Dmitry A. Kazakov
2012-06-25 16:43                                   ` Georg Bauhaus
2012-06-25 14:08                               ` stefan-lucks
2012-06-25 14:36                                 ` Dmitry A. Kazakov
2012-06-25 14:37                                   ` Dmitry A. Kazakov
2012-06-25 16:26                                   ` stefan-lucks
2012-06-25 19:42                                     ` Dmitry A. Kazakov
2012-06-26 11:50                                       ` stefan-lucks
2012-06-26 13:07                                         ` Dmitry A. Kazakov
2012-06-26 13:49                                           ` Georg Bauhaus
2012-06-26 14:45                                             ` Dmitry A. Kazakov
2012-06-26 16:48                                               ` Georg Bauhaus
2012-06-26 19:43                                                 ` Dmitry A. Kazakov
2012-06-27  8:23                                                   ` Georg Bauhaus
2012-06-27  8:52                                                     ` Dmitry A. Kazakov
2012-06-27 10:30                                                       ` Georg Bauhaus
2012-06-27 12:19                                                         ` Dmitry A. Kazakov
2012-06-27 13:41                                                           ` Nasser M. Abbasi
2012-06-28  7:00                                                             ` Georg Bauhaus
2012-06-27 15:08                                                           ` Georg Bauhaus
2012-06-29 21:03                                               ` Shark8 [this message]
2012-06-30  8:26                                                 ` Dmitry A. Kazakov
2012-06-30 12:54                                                   ` Niklas Holsti
2012-07-05  2:58                                                   ` Shark8
2012-07-05  7:24                                                     ` Dmitry A. Kazakov
2012-07-06  6:23                                                       ` Shark8
2012-07-06  7:57                                                         ` Dmitry A. Kazakov
2012-07-07  1:09                                                           ` Randy Brukardt
2012-07-07  8:44                                                             ` Dmitry A. Kazakov
2012-06-26 14:54                                           ` stefan-lucks
2012-06-26 15:14                                             ` Dmitry A. Kazakov
2012-07-03  5:28                                           ` Randy Brukardt
2012-07-03 12:53                                             ` Dmitry A. Kazakov
2012-07-03 13:48                                               ` Georg Bauhaus
2012-07-03 14:06                                                 ` Dmitry A. Kazakov
2012-07-03 16:12                                                   ` Georg Bauhaus
2012-07-03 16:45                                                     ` Georg Bauhaus
2012-07-05  1:45                                               ` Randy Brukardt
2012-07-05  7:48                                                 ` Dmitry A. Kazakov
2012-07-05 19:11                                                   ` Adam Beneschan
2012-07-05 19:55                                                     ` Dmitry A. Kazakov
2012-07-06  7:41                                                       ` Georg Bauhaus
2012-07-06  7:47                                                         ` Georg Bauhaus
2012-07-06  8:05                                                         ` Dmitry A. Kazakov
2012-07-06  8:30                                                           ` Georg Bauhaus
2012-07-06  9:01                                                             ` Dmitry A. Kazakov
2012-07-06 11:33                                                               ` Simon Wright
2012-07-06 13:25                                                                 ` Dmitry A. Kazakov
2012-07-06 12:07                                                               ` Georg Bauhaus
2012-07-06 13:37                                                                 ` Dmitry A. Kazakov
2012-07-06 16:17                                                                   ` Georg Bauhaus
2012-07-06 16:34                                                                   ` Georg Bauhaus
2012-07-06 19:18                                                                     ` Dmitry A. Kazakov
2012-07-07  1:24                                                                       ` Randy Brukardt
2012-07-07  9:09                                                                         ` Dmitry A. Kazakov
2012-07-07  1:18                                                                   ` Randy Brukardt
2012-07-07  9:14                                                                     ` Dmitry A. Kazakov
2012-07-07 12:06                                                                       ` Georg Bauhaus
2012-07-07 12:54                                                                         ` Dmitry A. Kazakov
2012-07-07 13:31                                                                           ` Georg Bauhaus
2012-07-03  5:10                                       ` Randy Brukardt
2012-07-03  4:51               ` Randy Brukardt
2012-07-03 12:46                 ` Dmitry A. Kazakov
2012-07-05  2:18                   ` Randy Brukardt
2012-07-05  8:48                     ` Dmitry A. Kazakov
2012-07-05 12:07                       ` Georg Bauhaus
2012-07-05 12:13                         ` Georg Bauhaus
2012-07-05 12:31                         ` Dmitry A. Kazakov
2012-07-05 18:16                           ` Georg Bauhaus
2012-07-05 19:57                             ` Dmitry A. Kazakov
2012-07-06  6:53                               ` Georg Bauhaus
2012-07-07  0:43                       ` Randy Brukardt
2012-07-07  8:06                         ` Dmitry A. Kazakov
2012-07-07 11:17                           ` Georg Bauhaus
2012-07-07 11:31                             ` Dmitry A. Kazakov
2012-07-07 12:21                               ` Georg Bauhaus
2012-07-07 13:03                                 ` Dmitry A. Kazakov
2012-06-20 19:18 ` Anh Vo
2012-06-20 20:16 ` Jeffrey R. Carter
2012-06-20 20:21   ` Jeffrey R. Carter
2012-06-20 20:51   ` Maciej Sobczak
2012-06-20 21:04     ` Dmitry A. Kazakov
2012-06-20 22:19   ` Robert A Duff
2012-06-21  6:32     ` Georg Bauhaus
2012-06-21 20:37   ` Randy Brukardt
2012-06-21 20:55     ` Jeffrey Carter
2012-06-22 19:15       ` Randy Brukardt
2012-06-21 20:23 ` Randy Brukardt
2012-06-22  7:34   ` Martin
replies disabled

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