Re: Ada 2012 Constraints (WRT an Ada IR)

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

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

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.

                             Randy.