Re: Ada 2012 Constraints (WRT an Ada IR)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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.

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

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de