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!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 13 Dec 2016 12:19:14 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32777 Date: 2016-12-13T12:19:14+01:00 List-Id: On 13/12/2016 11:39, G.B. wrote: > On 13/12/2016 09:27, Dmitry A. Kazakov wrote: > >>> No Ada in there. I was thinking of this posting. >> >> Ada is an object language here. Thus it can never be Ada. It could be >> a meta language of annotations for Ada, like SPARK. > > Pre doesn't have to be object language as has now been > said and confirmed a number of times. Being a part of the body it does not belong to declarations. >>>> Implied contracts are outside the scope. >>> >>> My point. Why should contracts not be explicit, in particular >>> when they had already been formal, albeit in a comment? >> >> Explicit contracts are only ones the framework can enforce, at all or >> pragmatically. > > Which role do programmers play in this? Are frameworks so much > better at proving and enforcing than humans? They are man made > frameworks after all, so whether they should necessarily limit > the scope of man seems dubious. You can translate Ada programs into machine instructions manually, if you feel yourself so superior. I prefer to to rely on frameworks. >> It is an explicit contract. > > Can you make it a Boolean expression? That depends on the language in question. It is not an expression in Ada and cannot be made one. > So, what are expected values for various inputs of A and B > passed to Plus_Too? Can this be stated? Yes it can and it is already done by the provided implementation of Plus_Too. This is exactly what implementations are for. You keep on confusing program behavior with statements about it. These are necessarily expressed in different frameworks and thus in different languages. It is impossible to mix them, that is a hard mathematical fact. >>> (Actually, there is no variable in the predicate other than those >>> implied in sub-expressions of Earth turning a black hole. >> >> Your fault. Formally no such predicate could even exist, merely due to >> Goedel incompleteness. > > Gödel's results do not apply to "+" in Standard.Integer, > so nothing is due to them here. They apply to a framework capable to spell all preconditions of "+". No such thing can exist. Therefore some [most] contracts will remain implied forever. > No proof can show bugs' absence whenever there is no predicate > describing expected values. Proofs show absence of bugs under the premise that all implied contracts hold. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de