From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Sat, 17 Dec 2016 10:13:17 +0100
Date: 2016-12-17T10:13:17+01:00 [thread overview]
Message-ID: <o32vjg$1jv4$1@gioia.aioe.org> (raw)
In-Reply-To: o31gke$jib$1@franka.jacob-sparre.dk
On 2016-12-16 20:51, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o3095a$1f4q$1@gioia.aioe.org...
>> On 15/12/2016 23:19, Randy Brukardt wrote:
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:o2tl62$1aro$1@gioia.aioe.org...
>>>> On 14/12/2016 23:53, Randy Brukardt wrote:
>>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>>> news:o2r1ca$184u$1@gioia.aioe.org...
>>>>> ...
>>>>>> Others tried to argue that such bodies are not bodies but magically
>>>>>> "preconditions". No, they are still bodies, just misplaced ones.
>>>>>
>>>>> Body /= implementation!! (Using "implementation" here in your sense as
>>>>> the
>>>>> entire execution of a subprogram.) A body is just the hidden part of
>>>>> the
>>>>> implementation; the part that is exposed to callers includes
>>>>> constraint,
>>>>> null exclusion, and predicate checks, and the precondition. The caller
>>>>> has a need to know about part of the implementation, and hopefully not
>>>>> about
>>>>> the rest. Exactly where the split between the specification and the
>>>>> body goes
>>>>> clearly depends on a need to know basis, and it has nothing to do with
>>>>> whether it is static or dynamic or provable.
>>>>
>>>> This pretty good summarizes why I consider it such a bad idea.
>>>
>>> The only alternative is to get rid of the separation of specifications and
>>> bodies (many languages do exactly that). Then you don't need any kind of
>>> contract.
>>
>> Exactly the opposite. Body /= implementation stance is getting rid of the
>> separation. And Ada is well along that path since Ada 05.
>
> The path was that set by Ada 83 with the idea of constraints. By your model,
> constraint checks belong to the implementation, and those have always been
> exposed in the specification.
Not explicitly. It is like the implementation of "+" when an integer
type declared. The implementation is assumed but not specified.
> Later versions of Ada have just built on this
> already existing (and very successful) idea, extending it to further cases.
I meant explicit code snippets in declarations, which includes "is
null", checks, etc.
It is very different from having type operations producing new
[sub]types like
subtype Y is X range 1..100;
or
type T is array (I) of E;
They declare and implement operations implicitly.
>>> Contracts that are too weak don't help; if a prover (or programmer!) has
>>> to look into the implementation (and that would necessarily be the case in
>>> your model), then there is no real separation.
>>
>> Surely they help. Moreover it is very important not to have to strong
>> contracts. The contract strength is how much the contract determines the
>> implementation. Too strong contracts prevent substitutability and thus
>> code reuse. Since any modification of a type breaks something somewhere.
>> Which is why contracts are relaxed in order to allow a range of
>> implementations, e.g. raising and handling exceptions etc.
>> Overspecification is a bad as underspecification.
>
> True enough. But irrelevant unless you're arguing for weak typing (and I
> know you're not doing that).
Typing is an example of usefulness of weak contracts. You just match
types and ignore the rest.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
next prev parent reply other threads:[~2016-12-17 9:13 UTC|newest]
Thread overview: 195+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-11-28 23:49 Ada 2012 Constraints (WRT an Ada IR) 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 [this message]
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
-- strict thread matches above, loose matches on Subject: below --
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-12-13 22:45 Randy Brukardt
2016-12-14 22:40 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
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
2016-12-21 22:03 Randy Brukardt
2016-12-21 23:02 ` Shark8
2016-12-21 22:12 Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox