Re: Ada 2012 Constraints (WRT an Ada IR)

["Randy Brukardt" <randy@rrsoftware.com>]

"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. Later versions of Ada have just built on this 
already existing (and very successful) idea, extending it to further cases.

>> 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).

                              Randy.