From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Fri, 16 Dec 2016 21:14:46 +0100
Date: 2016-12-16T21:14:46+01:00 [thread overview]
Message-ID: <o31hvm$1p4s$1@gioia.aioe.org> (raw)
In-Reply-To: o31gau$jd3$1@franka.jacob-sparre.dk
On 2016-12-16 20:46, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o309ac$1f4q$2@gioia.aioe.org...
>> On 15/12/2016 23:24, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o2tlcd$1aro$2@gioia.aioe.org...
>>>> On 14/12/2016 23:40, Randy Brukardt wrote:
>>>>> [Yet again had to break the thread because the thread has gotten too
>>>>> long
>>>>> to
>>>>> reply to - RLB]
>>>>>
>>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>>> news:o2s8l1$1fef$1@gioia.aioe.org...
>>>>>> On 2016-12-14 20:23, Shark8 wrote:
>>>>> ...
>>>>>>> You are observably wrong.
>>>>>>> If you supply a negative number, the body of X never executes.
>>>>>>
>>>>>> Of course it does. Semantically any effect of a call to X is due to
>>>>>> X's body. There is nothing else there.
>>>>>
>>>>> This is clearly false. The definition of the execution of a subprogram call
>>>>> (RM 6.4(10/2)) specifically says that the parameter associations are
>>>>> evaluated before the subprogram body is executed. 6.4.1 says that
>>>>> evaluation of the parameter associations include the conversion to the formal
>>>>> subtype - that conversion does the check that raises Constraint_Error.
>>>>
>>>> And semantically all this is a part of the body.
>>>
>>> I just quoted the rules in the RM that say specifically that it is not
>>> part of the body.
>>
>> What the problem? There is time to fix the RM wording. Call it "user
>> specified body" as opposed to the "body in effect".
>
> What possible good would it do?
It would fix wrong wording and eliminate misunderstanding about the
semantics of parameter checks and other prologues (and epilogues!) the
compiler uses to decorate the user body.
This is especially important for correctness proofs. A proof must take
into account *all* body. The user body part is not enough.
And with extensible bodies (as required by initialization, finalization
and aggregates) and the gluing code between them I don't know how are
you going to maintain this silly concept further...
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2016-12-16 20:14 UTC|newest]
Thread overview: 195+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-12-14 22:40 Ada 2012 Constraints (WRT an Ada IR) Randy Brukardt
2016-12-15 8:48 ` Dmitry A. Kazakov
2016-12-15 22:24 ` Randy Brukardt
2016-12-16 8:40 ` Dmitry A. Kazakov
2016-12-16 19:46 ` Randy Brukardt
2016-12-16 20:14 ` Dmitry A. Kazakov [this message]
2016-12-19 22:52 ` Randy Brukardt
2016-12-20 10:59 ` Dmitry A. Kazakov
2016-12-21 0:50 ` Randy Brukardt
2016-12-21 15:56 ` Dmitry A. Kazakov
-- strict thread matches above, loose matches on Subject: below --
2016-12-21 22:12 Randy Brukardt
2016-12-21 22:03 Randy Brukardt
2016-12-21 23:02 ` Shark8
2016-12-13 22:45 Randy Brukardt
2016-12-09 21:41 Randy Brukardt
2016-12-09 22:32 ` Niklas Holsti
2016-12-13 0:41 ` Randy Brukardt
2016-12-13 2:34 ` Shark8
2016-12-13 22:35 ` Randy Brukardt
2016-12-14 0:38 ` Shark8
2016-12-13 20:45 ` Niklas Holsti
2016-12-13 23:19 ` Randy Brukardt
2016-12-14 0:53 ` Shark8
2016-12-14 22:22 ` Randy Brukardt
2016-11-28 23:49 Shark8
2016-11-29 8:17 ` G.B.
2016-11-29 20:32 ` Shark8
2016-11-29 20:44 ` Dmitry A. Kazakov
2016-11-29 20:51 ` Shark8
2016-11-29 21:06 ` Dmitry A. Kazakov
2016-11-29 22:59 ` Shark8
2016-11-30 8:31 ` Dmitry A. Kazakov
2016-11-30 18:28 ` Shark8
2016-11-30 20:26 ` Niklas Holsti
2016-12-01 0:16 ` Shark8
2016-12-01 22:15 ` Randy Brukardt
2016-11-30 20:45 ` Dmitry A. Kazakov
2016-12-01 0:58 ` Shark8
2016-12-01 8:55 ` Dmitry A. Kazakov
2016-12-01 22:26 ` Randy Brukardt
2016-12-02 16:21 ` Dmitry A. Kazakov
2016-12-02 19:15 ` Randy Brukardt
2016-12-03 10:21 ` Dmitry A. Kazakov
2016-12-02 19:50 ` G.B.
2016-12-03 10:23 ` Dmitry A. Kazakov
2016-12-03 14:02 ` G.B.
2016-12-03 16:26 ` Dmitry A. Kazakov
2016-12-04 15:28 ` Robert Eachus
2016-12-05 8:41 ` Stefan.Lucks
2016-12-05 8:58 ` Dmitry A. Kazakov
2016-12-05 11:09 ` Simon Wright
2016-12-05 18:42 ` Shark8
2016-12-05 22:13 ` Dmitry A. Kazakov
2016-12-06 20:51 ` Shark8
2016-12-06 21:07 ` Dmitry A. Kazakov
2016-12-06 21:44 ` Shark8
2016-12-06 23:23 ` Randy Brukardt
2016-12-07 22:42 ` Shark8
2016-12-07 1:08 ` Dennis Lee Bieber
2016-12-07 6:36 ` Niklas Holsti
2016-12-07 13:10 ` Dennis Lee Bieber
2016-12-07 22:55 ` Brian Drummond
2016-12-08 2:44 ` Shark8
2016-12-07 10:04 ` G.B.
2016-12-07 10:14 ` G.B.
2016-12-07 10:51 ` J-P. Rosen
2016-12-08 18:33 ` G.B.
2016-12-09 8:26 ` J-P. Rosen
2016-12-09 8:56 ` G.B.
2016-12-10 15:13 ` Jacob Sparre Andersen
2016-12-11 19:50 ` Shark8
2016-12-05 22:07 ` Dmitry A. Kazakov
2016-12-06 23:09 ` Randy Brukardt
2016-12-07 10:03 ` Dmitry A. Kazakov
2016-12-07 22:37 ` Randy Brukardt
2016-12-08 8:46 ` Dmitry A. Kazakov
2016-12-10 15:24 ` Jacob Sparre Andersen
2016-12-09 9:12 ` Robert Eachus
2016-12-05 19:22 ` G.B.
2016-12-05 22:18 ` Dmitry A. Kazakov
2016-12-05 22:12 ` Randy Brukardt
2016-12-05 22:26 ` Dmitry A. Kazakov
2016-12-06 9:29 ` Simon Wright
2016-12-06 10:01 ` Dmitry A. Kazakov
2016-12-06 23:15 ` Randy Brukardt
2016-12-07 10:20 ` Dmitry A. Kazakov
2016-12-07 22:26 ` Randy Brukardt
2016-12-08 8:57 ` Dmitry A. Kazakov
2016-12-08 9:42 ` G.B.
2016-12-08 10:03 ` Dmitry A. Kazakov
2016-12-08 18:35 ` G.B.
2016-12-09 9:38 ` Dmitry A. Kazakov
2016-12-11 11:21 ` G.B.
2016-12-11 12:28 ` Dmitry A. Kazakov
2016-12-11 13:31 ` G.B.
2016-12-11 15:40 ` Dmitry A. Kazakov
2016-12-11 20:51 ` G.B.
2016-12-12 8:27 ` Dmitry A. Kazakov
2016-12-12 15:31 ` G.B.
2016-12-12 17:39 ` Dmitry A. Kazakov
2016-12-12 18:55 ` G.B.
2016-12-12 20:53 ` Dmitry A. Kazakov
2016-12-13 7:15 ` G.B.
2016-12-13 8:27 ` Dmitry A. Kazakov
2016-12-13 10:39 ` G.B.
2016-12-13 11:19 ` Dmitry A. Kazakov
2016-12-13 16:59 ` G.B.
2016-12-13 21:11 ` Dmitry A. Kazakov
2016-12-13 22:13 ` Shark8
2016-12-14 8:42 ` Dmitry A. Kazakov
2016-12-14 11:04 ` G.B.
2016-12-14 11:25 ` Dmitry A. Kazakov
2016-12-14 12:44 ` G.B.
2016-12-14 12:52 ` Dmitry A. Kazakov
2016-12-14 16:31 ` G.B.
2016-12-14 16:52 ` Dmitry A. Kazakov
2016-12-14 18:14 ` G.B.
2016-12-14 12:05 ` G.B.
2016-12-14 19:23 ` Shark8
2016-12-14 20:04 ` Dmitry A. Kazakov
2016-12-14 21:46 ` Shark8
2016-12-15 8:41 ` Dmitry A. Kazakov
2016-12-15 10:31 ` G.B.
2016-12-15 13:17 ` Dmitry A. Kazakov
2016-12-15 13:27 ` Dmitry A. Kazakov
2016-12-15 19:50 ` G.B.
2016-12-16 10:04 ` Dmitry A. Kazakov
2016-12-16 11:48 ` G.B.
2016-12-16 12:56 ` Stefan.Lucks
2016-12-16 19:59 ` Randy Brukardt
2016-12-16 20:35 ` G.B.
2016-12-17 9:33 ` Stefan.Lucks
2016-12-19 22:57 ` Randy Brukardt
2016-12-16 13:24 ` Dmitry A. Kazakov
2016-12-15 14:34 ` Shark8
2016-12-15 14:53 ` Dmitry A. Kazakov
2016-12-15 22:34 ` Shark8
2016-12-16 8:28 ` Dmitry A. Kazakov
2016-12-17 3:46 ` Shark8
2016-12-14 12:21 ` G.B.
2016-12-14 12:55 ` Dmitry A. Kazakov
2016-12-14 16:21 ` G.B.
2016-12-14 16:55 ` Dmitry A. Kazakov
2016-12-14 18:55 ` G.B.
2016-12-13 18:25 ` Shark8
2016-12-13 21:11 ` Dmitry A. Kazakov
2016-12-13 22:32 ` Shark8
2016-12-14 8:54 ` Dmitry A. Kazakov
2016-12-14 22:53 ` Randy Brukardt
2016-12-15 8:44 ` Dmitry A. Kazakov
2016-12-15 22:19 ` Randy Brukardt
2016-12-16 8:38 ` Dmitry A. Kazakov
2016-12-16 19:51 ` Randy Brukardt
2016-12-17 9:13 ` Dmitry A. Kazakov
2016-12-19 22:33 ` Randy Brukardt
2016-12-20 11:00 ` Dmitry A. Kazakov
2016-12-21 0:54 ` Shark8
2016-12-21 0:59 ` Randy Brukardt
2016-12-21 15:56 ` Dmitry A. Kazakov
2016-12-21 18:26 ` G.B.
2016-12-21 21:15 ` Dmitry A. Kazakov
2016-12-22 9:54 ` G.B.
2016-12-22 10:16 ` Dmitry A. Kazakov
2016-12-14 11:46 ` G.B.
2016-12-12 19:48 ` Shark8
2016-12-12 20:46 ` Dmitry A. Kazakov
2016-12-12 21:33 ` Shark8
2016-12-13 8:28 ` Dmitry A. Kazakov
2016-12-13 18:53 ` Shark8
2016-12-13 21:11 ` Dmitry A. Kazakov
2016-12-13 22:16 ` Shark8
2016-12-14 9:00 ` Dmitry A. Kazakov
2016-12-11 23:58 ` Paul Rubin
2016-12-12 8:33 ` Dmitry A. Kazakov
2016-12-12 15:23 ` G.B.
2016-12-12 15:51 ` G.B.
2016-12-09 21:46 ` Randy Brukardt
2016-12-13 11:56 ` Alejandro R. Mosteo
2016-12-13 15:02 ` Dmitry A. Kazakov
2016-12-13 17:38 ` Alejandro R. Mosteo
2016-12-05 22:06 ` Randy Brukardt
2016-11-29 17:53 ` Niklas Holsti
2016-11-29 18:21 ` Dmitry A. Kazakov
2016-11-29 20:45 ` Shark8
2016-11-30 0:03 ` Randy Brukardt
2016-11-30 0:59 ` Shark8
2016-12-01 10:33 ` AdaMagica
2016-11-29 23:52 ` Randy Brukardt
2016-11-30 1:24 ` Shark8
2016-11-30 22:12 ` Randy Brukardt
2016-11-30 1:29 ` Shark8
2016-11-30 22:17 ` Randy Brukardt
2016-12-01 1:21 ` Shark8
2016-12-01 22:07 ` Randy Brukardt
2016-12-01 10:06 ` AdaMagica
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox