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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!.POSTED!not-for-mail From: "G.B." Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Sat, 3 Dec 2016 15:02:17 +0100 Organization: A noiseless patient Spider Message-ID: References: <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com> <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com> <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Sat, 3 Dec 2016 14:01:04 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="0a9bcc5b0d9a1f414d9871f7c8587549"; logging-data="27074"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1817U2A/hwrh/Bjt1PhiBb+Y4cJm6eBXZ4=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 In-Reply-To: Cancel-Lock: sha1:ocRhggnSuV7+vRB6bJzl1vQjl84= Xref: news.eternal-september.org comp.lang.ada:32585 Date: 2016-12-03T15:02:17+01:00 List-Id: On 03.12.16 11:23, Dmitry A. Kazakov wrote: > On 2016-12-02 20:50, G.B. wrote: >> On 02.12.16 17:21, Dmitry A. Kazakov wrote: >>> Predicates are just arbitrary expressions the programmer sets without >>> understanding all effects of his actions. >> >> So are programs. > > When written in C? No, Ada. The question that you didn't answer was about how all normal Ada source texts can be known to express a fully proven program, by omitting assertions and replacing them with something else. Mind you, I don't think this would make sense either way: contracts based design IMHO is (a) for testing, (b) for description (e.g., guides for programmers), but not for expressing the solution. (This does not say anything yet about part-of or turned-off etc.) >> pragma Assert (Is_Sorted (S)); -- S a library level constant > You falsely assume that the effect of run-time assertion fault would be better than the effect of potential bug in any given context. Please don't put assumptions into my context. There will be no run-time assertions caused by this Assert. Guess why? The joint assertion and build process have fixed a bug for sure. It is proven to be gone. The bug was discovered by formalizing an already existing informal predicate. The now formal predicate, will be ignored at run-time. As before. >> Now, do assertion distract from learning how to write correct >> programs using types that manage to express them? > > Yes they do. Maybe, but without knowing predicates, one will never know what "correct" stands for. Correct programs need the preparatory work of asserting, I think. >> And in such >> a way that an Ada compiler can determine truth at compile time? > > This is not how predicates work So? > and has nothing to do with truth. Predicates, a.k.a. all Boolean expressions, are our only way of making statements that can be true or not. Or so I have learned. -- "HOTDOGS ARE NOT BOOKMARKS" Springfield Elementary teaching staff