From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Thu, 15 Dec 2016 16:19:04 -0600
Organization: JSA Research & Innovation
Message-ID: <o2v4so$5ik$1@franka.jacob-sparre.dk>
References: <c06ee4e6-d616-4e01-ba2e-cb111a81f6f6@googlegroups.com>
   <o27gpr$o8k$1@franka.jacob-sparre.dk> <o28non$1fn8$1@gioia.aioe.org>
 <o2a2ad$vnp$1@franka.jacob-sparre.dk> <o2b79r$1dit$1@gioia.aioe.org>
 <o2b9rg$ejl$1@dont-email.me> <o2bb4o$1jpb$1@gioia.aioe.org>
 <o2c93i$rpp$2@dont-email.me> <o2du2t$1ghu$1@gioia.aioe.org>
 <o2jcpd$75p$1@dont-email.me> <o2jgom$18jg$1@gioia.aioe.org>
 <o2jkdm$bt$1@dont-email.me> <o2js2d$1qh4$1@gioia.aioe.org>
 <o2ke6d$gcs$1@dont-email.me> <o2ln13$et0$1@gioia.aioe.org>
 <o2mfpc$ttp$1@dont-email.me> <o2mncc$gjn$1@gioia.aioe.org>
 <o2mroh$dsk$1@dont-email.me> <o2n2o1$1515$1@gioia.aioe.org>
 <o2o73n$ci1$1@dont-email.me> <o2obed$qkk$1@gioia.aioe.org>
 <o2oj2u$i8h$1@dont-email.me> <o2olfi$1ca9$1@gioia.aioe.org>
 <1af458a8-cf5b-4dd7-824d-eed1ed5ffb21@googlegroups.com>
 <o2po6q$1hnq$3@gioia.aioe.org>
 <b43e7e36-769a-4546-87aa-c2d2c790525d@googlegroups.com>
 <o2r1ca$184u$1@gioia.aioe.org> <o2sign$lj1$1@franka.jacob-sparre.dk>
 <o2tl62$1aro$1@gioia.aioe.org>
NNTP-Posting-Host: rrsoftware.com
X-Trace: franka.jacob-sparre.dk 1481840344 5716 24.196.82.226 (15 Dec 2016
 22:19:04 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Thu, 15 Dec 2016 22:19:04 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
X-RFC2646: Format=Flowed; Response
Xref: news.eternal-september.org comp.lang.ada:32858
Date: 2016-12-15T16:19:04-06:00
List-Id: <comp.lang.ada>

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