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: Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Fri, 24 Apr 2015 17:26:43 -0500 Newsgroups: comp.lang.ada Date: Fri, 24 Apr 2015 18:26:41 -0400 From: Peter Chapin X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu Subject: Re: {Pre,Post}conditions and side effects In-Reply-To: <87tww5296f.fsf@adaheads.sparre-andersen.dk> 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-3qWcbohC6C/wy7g47wA6OBBTOVSyFWWzB45Ao7Ok3vCh3HHJtOY23HtAvN3Hd12pr8KlFGqHkK4i9uQ!5827uqxNOiss2AtjT24WhPQ2FTxltP0ubMxR3NY0gcf5TyCA4g01F/gck9anLEFd9B3BAJypozN0!9jfHID+3LWdx0tohdQ== 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: 4837 Xref: number.nntp.giganews.com comp.lang.ada:192910 Date: 2015-04-24T18:26:41-04:00 List-Id: On Fri, 24 Apr 2015, Jacob Sparre Andersen wrote: > But when are you putting "essential program logic" in an assertion? I think a servicable rule is this: If the program works as required, with all necessary checks still present, with all assertions removed, then we can say the assertions contain no essential program logic. In a correct program all assertions should always be true. > 1) subtype Non_Negative_Matrix is Ada.Numerics.Real_Arrays.Real_Matrix > with Dynamic_Predicate > => (Non_Negative_Matrix'First (1) = 1) and > (Non_Negative_Matrix'First (2) = 1) and > (for all E of Non_Negative_Matrix => E >= 0.0); Although the Dynamic_Predicate asserts that the matrix elements are all non-negative, this does not remove the program's obligation to include checks that no negative elements are added to the matrix. The assertion only exists to catch mistakes in those checks. It does not exist to actually *be* those checks. In that respect the assertion is not "essential program logic." > 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. > 3) function Binary_Search (Source : in List; > Key : in Keys) return Values > with Pre => Sort (Source); -- Sorts Source if it isn't already sorted. Yes, definitely wrong. On the other hand using something like with Pre => Is_Sorted(Source); could be reasonable. > I consider examples (1) and (2) fine, but example (3) a very bad idea. I agree that (1) and (2) are fine, but that doesn't mean the program should rely on the assertions for its proper functioning. The assertions check correctness; they don't implement it. Even if the assertions are removed, the program should still execute properly. > But I dislike banning "essential program logic" in assertions, as any > assertion is program logic. And if it isn't essential, why should it be > there? Because we often make mistakes and it's nice to have our thinking double checked. Also, of course, the assertions make our intentions known to tools, such as SPARK, that can automatically verify our code implements the conditions we are asserting. > One problem I have with assertion aspects is that I get the same > exception no matter which mistake I have made. If I put the check > inside a subprogram instead of in its profile, I can get more clear > information about which kinds of mistakes I make. Putting the check inside the subprogram is quite a different thing. That is part of your implementation of correctness. Since assertions should never fail, using the same exception for all of them isn't terrible. That said, the upcoming feature that allows different exceptions to be used when an assertion fails is nice too. Peter