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!mx02.eternal-september.org!.POSTED!not-for-mail From: Georg Bauhaus Newsgroups: comp.lang.ada Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io Date: Wed, 28 Oct 2015 12:06:33 +0100 Organization: A noiseless patient Spider Message-ID: References: <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net> <87pp0030c1.fsf@theworld.com> <135hiczk56x02.1xixcme8btbl4.dlg@40tude.net> <1dzlgoh4u2j7t$.1un3dfy0oeigd$.dlg@40tude.net> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Wed, 28 Oct 2015 11:04:26 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="165a9bd5b26d138768453b035288e461"; logging-data="30248"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/mipT19K475bqzi8sAfMs9YLy9uSiWBk4=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0) Gecko/20100101 Thunderbird/38.3.0 In-Reply-To: <1dzlgoh4u2j7t$.1un3dfy0oeigd$.dlg@40tude.net> Cancel-Lock: sha1:/C1nsTZqZE73dbEJqs2GzBNlIog= Xref: news.eternal-september.org comp.lang.ada:28085 Date: 2015-10-28T12:06:33+01:00 List-Id: On 27.10.15 21:04, Dmitry A. Kazakov wrote: > On Tue, 27 Oct 2015 17:43:36 +0100, G.B. wrote: > >> On 27.10.15 16:26, Dmitry A. Kazakov wrote: >>> How do you know if some callers would not appreciate Status_Error as >>> a possible outcome? >> >> Actually, this situation is what contracts are made for, >> I think: >> as a caller, you say what you want the procedure to do, >> or else you don't sign this contract. I.e., a redesign >> via ECR is in order before you sign. > > Sure, except that you don't subscribe the contract you cannot fulfill. Yes, an impasse is a possible situation when negotiating contracts. The interests of the business people will give way to at least one resolution. > The point can be summarized this way. If an exception is a part of the > contract then Status_Error is much better than Constraint_Error "Better than Assertion_Error?" I understand we are going to get subtype Open_File is File with Predicate => Is_Open(Open_File) or else raise Status_Error with "..."; If the Predicate is associated with a subtype, the "specializing" message after WITH cannot very special. It can be more special when associated with a subprogram, though. But it can be special in any case. > If the contract is not to raise, then, firstly, there is no > way to enforce it, Enforcing it appears possible in the above case, at least for each single program involving file objects, IIUC. > and, secondly, if there were a way, proving no > Status_Error would be no harder than no Constraint_Error. Ergo, no use. Whenever one defines "use" to have the same meaning as "proof", then the argument is an elaborate tautology. Now that will be an almost useless definition 8-) However, another use of predicates is to document assumptions. If the assumptions are correct, but the compiler cannot determine their truth, should we hide the assumptions? Is it possible to redesign the subtypes etc below, making them private types instead, so that the compiler "knows" all objects to have the desired properties? What's the impact on O(?)? package Conj is -- -- dumb tests; we actually know all the numbers, the point is -- to be able to refer to them in assumptions, for the contract. -- subtype Candidate is Positive range 2 .. Positive'Last; function Is_Prime (N : Candidate) return Boolean is (not (for Some X in 2 .. Candidate'Pred(N) => N rem X = 0)); subtype Known_Range is Natural range 0 .. Natural'Min (Natural'Last, 4 * 10**17); subtype GN is Known_Range with Predicate => -- dynamic (if GN >= 4 and GN rem 2 = 0 then (for Some A in 2 .. GN => (for Some B in 2 .. GN => Is_Prime (A) and Is_Prime (B) and GN = A + B))); end Conj; Running an unnecessary test may burn a CPU core, with Conj; procedure Test_Conj is Test : constant Conj.GN := 1234567890; begin null; end Test_Conj;