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!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Fri, 24 Apr 2015 20:01:02 -0500 Newsgroups: comp.lang.ada Date: Fri, 24 Apr 2015 21:01:00 -0400 From: Peter Chapin X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu Subject: Re: {Pre,Post}conditions and side effects In-Reply-To: Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> User-Agent: Alpine 2.11 (CYG 23 2013-08-11) Organization: Vermont Technical College MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-VOwwyFyfPyCH7if2T164zI8RwjhSM1xMS6p/AFYSu+I9k9wsmq0zq5PsBFJlHBhWN3r1VAIWXW78AS3!v/QSRUF01nt61SqnTdOEwmiW1GHv6ewDe7D+SWBDtm2Lmy04nwU2x5akTCtsRvFdqMVDr1Wdomfm!NuyTzZC+Y62aCyaVnQ== X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 4373 Xref: news.eternal-september.org comp.lang.ada:25609 Date: 2015-04-24T21:01:00-04:00 List-Id: On Fri, 24 Apr 2015, Randy Brukardt wrote: >>> 2) procedure New_Line (File : in File_Type) >>> with Pre => Is_Open (File) and then >>> Mode (File) in (Out_File | Append_File); >> >> Similarly here the program is still obligated to only pass File objects to >> New_Line that represent open files. If the program accidentally passes an >> unopened file to New_Line the assertion will catch the logical error. >> However, the assertion should not take the place of earlier checks. Again >> the assertion is not essential program logic. > > I definitely disagree here. This example is essentially similar to the one > given in the upcoming Corrigendum (3.2.4(41-51/4). In a case like this, the > precondition (or predicates as in the example) *replace* the checks required > by English text in the RM. There would no internal checks of correctness. In this case it's not the internal checks I mean. Hoisting the internal checks into preconditions makes sense to me, at least in certain (many?) cases. In my comments above I'm talking about checks occurring before New_Line is called. Somewhere the programmer tried to open a file. If the programmer attempts to call New_Line without first verifying that the file opened successfully, that's a logical error in the program. Checking that Is_Open(File) is true provides some protection against such an error... regardless of if the check is a precondition or done inside the body of New_Line. Either way, in a correct program that check should never fail. The beauty of doing it in a precondition is that the "unnecessary" check can be removed by changing the assertion policy. In contrast imagine a procedure that takes file and does some processing on it. Suppose the procedure raises some exception if the file has the wrong format. The programmer might decide that it's not wrong to call the procedure with an incorrectly formatted file, and let that be a matter for the procedure to worry about. In that case, adding the check as a precondition doesn't seem right; a correct program might call the procedure with a badly formatted file. On the other hand if the programmer decides it's illogical to call the procedure with an incorrectly formatted file because the file has (supposedly) been verified previously, using a precondition to check the format makes sense. Same procedure, same check... the sensibility of making the check a precondition depends on the context in which the procedure is used. In the first case the caller relies on the procedure to do the check. In the second case the procedure relies on the caller to do it. Ultimately it ends up being a design decision. Peter