!standard A.18.3(16.1/5) 20-03-06 AI12-0370-1/01 !class Presentation 20-03-06 !status work item 20-03-06 !status received 20-02-10 !priority Low !difficulty Easy !subject Pattern to use for specifying a precondition !summary When possible, a part of a precondition that raises a particular exception should be specified in the form: (not ) or else raise If the can be inverted (as is possible by replacing a relational operator with a different one), then the "not" and parenthesis can be omitted. !problem Some of the proposed preconditions in the Standard are written as cascaded if statements. For instance, A.18.3(16.1/5) says: procedure Query_Element (Container : in List; Position : in Cursor; Process : not null access procedure (Element : in Element_Type)) with Pre => (if Position = No_Element then raise Constraint_Error elsif not Has_Element (Container, Position) then raise Program_Error); This seems backwards to the purpose of a precondition, which is to specify what is allowed for a call (as opposed to what is *not* allowed). This would be better written: procedure Query_Element (Container : in List; Position : in Cursor; Process : not null access procedure (Element : in Element_Type)) with Pre => (Position /= No_Element or else raise Constraint_Error) and then (Has_Element (Container, Position) or else raise Program_Error); !proposal (See Summary.) !discussion Many of the preconditions are relatively direct translations of the English text that they are replacing. These are often written in terms of what the body needs to do, which is typically a cascaded if statement. Still, the extra effort to write the preconditions in the form of what is allowed is preferable. --- If we were willing to change the exceptions raised, many proposed preconditions could be simplified. For instance, in the example given here, Has_Element returns False for Position = No_Element, so a single test could be done if we were willing to change the exception from Constraint_Error to Program_Error (or vice-versa). --- Note that this AI is just instructions to the editor; it does not directly make any changes to the Standard. [Editor: I note that strictly following this would require inverting almost all of the existing preconditions for the containers; the preconditions primarily use the "if then raise " form as that directly matches the English wording that is being replaced. Replacing all of that with "(not ) or else raise " is likely to have many mistakes (due to the large number of changes needed and the difficulty of getting "not" correctly positioned and associated). It also will take a substantial amount of time, in particular because all of the manually inserted line breaks will have to be moved. This would have a substantial impact on our budget.] !example One of the original Delete definitions for Vectors is: procedure Delete (Container : in out Vector; Position : in out Cursor; Count : in Count_Type := 1); If Position equals No_Element, then Constraint_Error is propagated. If Position does not designate an element in Container, then Program_Error is propagated. Otherwise, Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. --- All of the text in front of "Otherwise" belongs to the precondition. We also have to deal with tampering in the precondition. The direct translation of the rules resulted in the following: procedure Delete (Container : in out Vector; Position : in out Cursor; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error elsif Position = No_Element then raise Constraint_Error elsif not Has_Element (Container, Position) then raise Program_Error), Post => Length (Container)'Old - Count <= Length (Container) and then Position = No_Element; Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. --- To follow the recommendation of this AI, we need to restructure the Precondition to: procedure Delete (Container : in out Vector; Position : in out Cursor; Count : in Count_Type := 1) with Pre => ((not Tampering_With_Cursors_Prohibited (Container)) or else raise Program_Error) and then (Position /= No_Element or else raise Constraint_Error) and then (Has_Element (Container, Position) or else raise Program_Error), Post => Length (Container)'Old - Count <= Length (Container) and then Position = No_Element; Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. The mixture of "and then" and "or else" force additional parentheses and make the correspondence to the original text much less clear. But it does have the advantage of more clearly specifying what is required (assuming that the reader doesn't get confused by all of the boolean operations - if the idiom is common enough that concern should be reduced). !ASIS No ASIS changes needed. !ACATS test No ACATS tests needed specifically for this. !appendix From: Randy Brukardt Sent: Monday, February 10, 2020 11:35 PM [Part of and eventually split from another thread - see AI12-0366-1 for that thread - Editor.] This precondition changes the exception raised from Constraint_Error to Assertion_Error. The exception raised might not matter to SPARK, but for Ada it should be either Constraint_Error or Program_Error. (That is the case for the "regular" integers as well, if you're really trying to match that behavior.) I think it would be better to be Program_Error (use of an invalid value), but 13.9.1(9) allows either. In any case, the exception needs to be reflected in this precondition and all of the others as well: function "+" (L : Big_Integer) return Big_Integer with Pre => (if Is_Valid (L) then raise Program_Error); **************************************************************** From: Jean-Pierre Rosen Sent: Monday, February 10, 2020 11:58 PM > function "+" (L : Big_Integer) return Big_Integer > with Pre => (if Is_Valid (L) then raise Program_Error); with Pre => (if {not} Is_Valid (L) then raise Program_Error); Presumably ;-) **************************************************************** From: Randy Brukardt Sent: Tuesday, February 11, 2020 2:01 AM > with Pre => (if {not} Is_Valid (L) then raise Program_Error); > Presumably ;-) Just checking if anyone is reading carefully. ;-) **************************************************************** From: Tucker Taft Sent: Tuesday, February 11, 2020 7:09 AM An alternative pattern that might be preferable is: with Pre => Is_Valid(L) or else raise Program_Error; You don't need the parentheses in this pattern, and it is perhaps easier to understand because it is stated more positively. **************************************************************** From: Randy Brukardt Sent: Tuesday, February 11, 2020 4:53 PM > An alternative pattern that might be preferable is: > > with Pre => Is_Valid(L) or else raise Program_Error; > > You don't need the parentheses in this pattern, and it is perhaps > easier to understand because it is stated more positively. I thought about that, but then had to stop to remember the truth tables to determine if I had the right short circuit operation. I figured that if it takes that much mental energy to figure out if it is right, it isn't very readable for the uninitiated, either, so I wrote it with an if expression, which is easily understandable to all. (At least if I put in the "not". ;-) **************************************************************** From: Tucker Taft Sent: Tuesday, February 11, 2020 9:30 PM Interesting. To me, it feels backwards to write "Pre => (not Is_Valid(L) then raise ...)" when the precondition would be "Pre => Is_Valid(L)" if you didn't need to specify the exception. I read the "or else" very naturally as what action to take if the precondition fails. With the "Pre => (if not P then raise ...)" pattern I find myself asking "exactly what *is* the precondition"? It seems to have disappeared or been inverted. I'd be curious how others react. Presumably we need to pick a pattern and stick with it throughout the RM ... **************************************************************** From: Richard Wai Sent: Tuesday, February 11, 2020 9:34 PM I have to agree with Tuck here – “Is_Valid (L) or else raise Program_Error” reads really nicely. **************************************************************** From: Gary Dismukes Sent: Tuesday, February 11, 2020 10:01 PM I feel the same way. **************************************************************** From: Jean-Pierre Rosen Sent: Wednesday, February 12, 2020 12:34 AM > I'd be curious how others react.  Presumably we need to pick a pattern > and stick with it throughout the RM ... I'm also in favor of "or else", on the ground that positive conditions are less error prone than negative ones (and Randy proved it!). **************************************************************** From: Bob Duff Sent: Wednesday, February 12, 2020 6:51 AM > I'd be curious how others react. Same as you. **************************************************************** From: Edmond Schonberg Sent: Wednesday, February 12, 2020 6:58 AM Concur. **************************************************************** From: Erhard Ploedereder Sent: Wednesday, February 12, 2020 3:28 PM I am all in favor of Pre => theRealPre or else raise A_Raucus i.e. Tuck's version. Stylistically, the "or else" should become an idiom to always be added for non-True real PreConds. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 12, 2020 7:09 PM I worried about this with the containers and came to the opposite conclusion, but mainly because this does not extend well. In the containers, there are multiple conditions each raising different exceptions. This to me is the norm for Ada packages (Text_IO, Claw, and most of the other stuff I can think of raise multiple different exceptions on failures). Moreover, in a real package, these different failures all have different exception messages, so lumping everything into one raise would definitely be losing information. I started using the "or else" formulation for some of the checks in the containers, but it got messy quick. I eventually went back and changed them all (I think) to the "if" formulation for consistency. >I'd be curious how others react. Presumably we need to pick a pattern >and stick with it throughout the RM ... This fills me with dread. I would have to spend upwards of 40 hours to redo the containers in this form, and I'd expect the result to be stuffed full of errors (wrong exception, wrong order of checks, etc.) If we wanted to make such a suggestion for *new* packages, it might make sense (depending on how important raising multiple exceptions is and how important targeting exception messages is). I don't think it makes sense when the precondition is modeling an existing package, especially one with lots of "if xxx, then raise yyy" text to model. Appendix: An example from the containers. One of the original Delete definitions for Vectors is: procedure Delete (Container : in out Vector; Position : in out Cursor; Count : in Count_Type := 1); If Position equals No_Element, then Constraint_Error is propagated. If Position does not designate an element in Container, then Program_Error is propagated. Otherwise, Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. --- All of the stuff in front of "Otherwise" belongs to the precondition. We also have to deal with tampering in the precondition. (Other routines like Insert also have an overlength precondition - that's another rule that is "implicit", like tampering.) I ended up with the following: procedure Delete (Container : in out Vector; Position : in out Cursor; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error elsif Position = No_Element then raise Constraint_Error elsif not Has_Element (Container, Position) then raise Program_Error), Post => Length (Container)'Old - Count <= Length (Container) and then Position = No_Element; Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. --- Note that in a real implementation, there would be a message associated with each of the raise expressions (or possibly they'd be replaced by a no-return function call that constructed a message). If we truly didn't care about exceptions, we could have simply replaced this by with Pre => (not Tampering_With_Cursors_Prohibited (Container)) and then Has_Element (Container, Position) but that would be inconsistent in that it would change the exception raised and be unfriendly to the Ada user by no longer telling them what happened when they inevitably make a mistake. I did consider wrapping the rather common part (if Position = No_Element then raise Constraint_Error elsif not Has_Element (Container, Position) then raise Program_Error) into a subprogram, but we had just rejected doing that for Annex D subprograms and I didn't want to do the same thing here. And it sounds like the SPARK people would have heartburn with those sorts of abstractions. **************************************************************** From: Richard Wai Sent: Wednesday, February 12, 2020 7:18 PM > procedure Delete (Container : in out Vector; > Position : in out Cursor; > Count : in Count_Type := 1) > with Pre => (if Tampering_With_Cursors_Prohibited (Container) > then raise Program_Error > elsif Position = No_Element then raise Constraint_Error > elsif not Has_Element (Container, Position) > then raise Program_Error), > Post => Length (Container)'Old - Count <= Length (Container) and then > Position = No_Element; > > Delete (Container, To_Index (Position), Count) is called, and then Position is > set to No_Element. In this kind of case I think what you have there is quite ideal. I don't think we should be making any general rule in regards to "or else". I think the goal of any given pre/post condition should simply be clarity and readability. In the particular example of Is_Valid(X) or else raise Program_Error, this was nice, clean, and readable. In the above contracts, they are also quite readable and clean, so I don't see why we'd need to change it.. I don't see what's wrong with a case-by-case approach, converging on the higher-level ideals of readability and clarity only. **************************************************************** From: Tucker Taft Sent: Wednesday, February 12, 2020 8:20 PM The "or else" can be used for a sequence of conditions as well, though it is perhaps not as clear of a win: with Pre => (not Tampering_With_Cursors_Prohibited (Container) or else Program_Error) and then (Position /= No_Element or else raise Constraint_Error) and then (Has_Element (Container, Position) or else raise Program_Error), I think I still prefer this "or else" pattern, personally, even when there are multiple conditions as in this case. Note that if we didn't care which exception was raised, we would presumably write: with Pre => not Tampering_With_Cursors_Prohibited (Container) and then Position /= No_Element and then Has_Element (Container, Position), So the "or else" pattern still has the advantage of more closely matching the "simple" specification of the preconditions. **************************************************************** From: Randy Brukardt Sent: Wednesday, February 12, 2020 8:42 PM > The "or else" can be used for a sequence of conditions as well, though > it is perhaps not as clear of a win: > > with Pre => > (not Tampering_With_Cursors_Prohibited (Container) or else > Program_Error) > and then > (Position /= No_Element or else raise Constraint_Error) > and then > (Has_Element (Container, Position) or else raise Program_Error), > > I think I still prefer this "or else" pattern, personally, even when > there are multiple conditions as in this case. Is this even right??? Doesn't an exception get raised if any one of these is True? That's the problem I have - when I read the above I literally have no idea what it does unless I work out the truth tables. That's not useful to me. I get DeMorgan wrong at least 2/3rds of the time, even though I'm really aware of it (part of the reason I get it wrong is *because* I'm aware of it; sometimes I apply it twice!) If I have to change the hundreds of preconditions into this form, there will be literally hundreds of mistakes. There is literally no chance that I will do it right (one of the reasons I added quality warnings to Janus/Ada was because of DeMorgan problems - I've found at least 6 of those in existing code that presumably wasn't tested enough. I wanted to catch those much earlier when possible to save debugging). In any case, it is much less clear that the above matches the wording that it replaced. And that was my #1 concern with these (not introducing bugs), I was less concerned about the readability. I suppose that could fall under the "don't make new stuff look grafted on" Tucker meta-rule. > Note that if we didn't care which exception was raised, we would > presumably write: > > with Pre => > not Tampering_With_Cursors_Prohibited (Container) > and then > Position /= No_Element > and then > Has_Element (Container, Position), > > So the "or else" pattern still has the advantage of more closely > matching the "simple" specification of the preconditions. Well, Has_Element returns False for a null Position, the only reason it is mentioned separately is to give the correct exception. So you would *not* mention that separately. (I debated about asking to change the exception so Has_Element would only need to be mentioned once, but it seems too common to change without breaking someone's exception handler.) Also, I always parentheses "not" because it's never clear how it associates. Even if is "right" from a language perspective, a reader needs the help. Since the "if" already has parens you can't see that in my above example. with Pre => (not Tampering_With_Cursors_Prohibited (Container)) and then Has_Element (Container, Position), And I would have preferred to use prefix notation with these calls (but the ARG said no): with Pre => (not Container.Tampering_With_Cursors_Prohibited) and then Container.Has_Element (Position), In any case, redoing these would also mean redoing all of the line length fixes that are needed to get these to fit on an RM page properly. It would definitely take many, many hours to do. I'm not at all sure I want to ask AdaCore for more money to pour in this particular rat-hole. **************************************************************** From: Jean-Pierre Rosen Sent: Thursday, February 13, 2020 12:07 AM > The "or else" can be used for a sequence of conditions as well, though it is > perhaps not as clear of a win: > > with Pre => > (not Tampering_With_Cursors_Prohibited (Container) or else Program_Error) > and then > (Position /= No_Element or else raise Constraint_Error) > and then > (Has_Element (Container, Position) or else raise Program_Error), But then you have negative conditions, and this is very error-prone. There is non one-fit-all rule for readability; in this case, I prefer the if-expression. **************************************************************** From: Tucker Taft Sent: Thursday, February 13, 2020 9:24 AM >> The "or else" can be used for a sequence of conditions as well, though it >> is perhaps not as clear of a win: >> with Pre => >> (not Tampering_With_Cursors_Prohibited (Container) or else Program_Error) >> and then >> (Position /= No_Element or else raise Constraint_Error) >> and then >> (Has_Element (Container, Position) or else raise Program_Error), > But then you have negative conditions, and this is very error-prone. Can you clarify? The "if/elsif" version was: with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error elsif Position = No_Element then raise Constraint_Error elsif not Has_Element (Container, Position) then raise Program_Error), Here you have "not Has_Element" whereas with "or else" you have "Has_Element" (which is the actual precondition). Admittedly with "if/elsif" you have "Tampering_With_Cursors_Prohibited" rather than "not Tampering_With_Cursors_Prohibited," but again the actual precondition is "not Tampering_With_Cursors_Prohibited." So can you clarify what you mean by "negative conditions"? Note that in the English descriptions, we typically describe what should be true at the point of the call, and then say that if such a check fails, NNN_Error is raised. Using the "or else" pattern more nearly matches the past English descriptions. > There is non one-fit-all rule for readability; in this case, I prefer > the if-expression. We could settle on using "if/elsif" when there are multiple conditions, and "or else" if there is only one, but I am not convinced that makes sense. I do accept Randy's argument that redoing all of the existing ones in the Containers would be a pain, and if we really decide we want to do this someone else ought to volunteer to do the shift over (e.g. me ;-). **************************************************************** From: Jean-Pierre Rosen Sent: Thursday, February 13, 2020 9:52 AM > Note that in the English descriptions, we typically describe what > should be true at the point of the call, and then say that if such a > check fails, NNN_Error is raised.  Using the "or else" pattern more > nearly matches the past English descriptions. > It's really double negations (or close to) that I tend to avoid. not Tampering_with_cursors_prohibited => hmmmmmm oh yes, it's allowed position /= No_Element => hmm oh yes, the position designates an element not has_element does not have this aspect of double negation. In any case readability is really a matter of appreciation (except for the universal rule: "what I write is readable, what you write is not readable") But I'd rather not have a systematic rule, rather on case-by-case **************************************************************** From: Tucker Taft Sent: Thursday, February 13, 2020 10:08 AM > But I'd rather not have a systematic rule, rather on case-by-case I don't think that is really practical. I think we should at least try to have a general rule or rules, which could leave some room for exceptions, but which we would only use if the general rule produces something unintelligible. I also wonder whether some judicious use of subtype predicates might help, e.g. for the tampering stuff: subtype Updatable_Map is Map with Dynamic_Predicate => not Tampering_With_Cursors_Prohibited (Updatable_Map), Predicate_Failure => raise Program_Error; and we could use these directly as parameter subtypes, or use them in preconditions as: with Pre => (Container in Updatable_Map or else raise Program_Error) and then ... thereby eliminating the double negative. **************************************************************** From: Richard Wai Sent: Thursday, February 13, 2020 2:09 PM >> But I'd rather not have a systematic rule, rather on case-by-case > I don't think that is really practical. I think we should at least try to > have a general rule or rules, which could leave some room for exceptions, > but which we would only use if the general rule produces something > unintelligible. I also wonder whether some judicious use of subtype > predicates might help, e.g. for the tampering stuff: Maybe this calls for something less of a “rule”, and more a guideline – like a design standard for contracts in the RM. I agree that we should aim for some kind of consistency, though I don’t think there will be any specific set of rule that can optimize for human readability. Maybe some general guidelines such as preferring the affirmative where possible (Is_Valid or else rather than if not Is_Valid then), and to use of short circuits in preference to if and case statements, unless where there is a clear “fan-out” of conditions. Something like that.. **************************************************************** From: Randy Brukardt Sent: Thursday, February 13, 2020 5:19 PM ... >I don't think that is really practical. I think we should at least try >to have a general rule or rules, which could leave some room for >exceptions, but which we would only use if the general rule produces >something unintelligible. I do agree with this, but I thought we did that *before* I did the containers. Apparently not. :-( >I also wonder whether some judicious use of subtype predicates might >help, e.g. for the tampering stuff: > > subtype Updatable_Map is Map > with > Dynamic_Predicate => > not Tampering_With_Cursors_Prohibited (Updatable_Map), > Predicate_Failure => raise Program_Error; > > and we could use these directly as parameter subtypes, This doesn't work for at least two reasons: (1) It would change the profile in cases where subtype conformance is required ('Access, renames-as-body, etc.) That's a compatibility issue, a relatively minor one but not justifiable for what is just a more formal restating of the semantics; (2) Containers are tagged, and controlling parameters have to be the first subtype. Steve was trying to lift that restriction, but everyone hated his solution and it was given to Bob to deal with. (I suppose you could volunteer to attempt a fix to this issue, since you're done with your homework. It's AI12-0243-1.) It also seems that the SPARK people don't like this technique (although that may be more of an education issue than a real problem). >or use them in preconditions as: > > with Pre => > (Container in Updatable_Map or else raise Program_Error) > and then > ... > > thereby eliminating the double negative. This doesn't seem to buy much. One could simply reverse the sense of the function Tampering_With_Cursors_Prohibited (since it is new and exists mainly to support preconditions), and call it Tampering_With_Cursors_Allowed instead. Of course, all of the wording related to it would also have to be swapped, which would bring its own set of work. **************************************************************** From: Randy Brukardt Sent: Thursday, February 13, 2020 5:29 PM ... >Note that in the English descriptions, we typically describe what >should be true at the point of the call, and then say that if such a >check fails, NNN_Error is raised. Using the "or else" pattern more >nearly matches the past English descriptions. That's certainly *not* the style of the containers. They're described in terms of what the body does. As in the example I gave of Delete: If Position equals No_Element, then Constraint_Error is propagated. If Position does not designate an element in Container, then Program_Error is propagated. Otherwise, Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. I don't know if this proves much other than the way *I* think (since I wrote many of these descriptions, many years ago), but translating them to a precondition in the style you want would require inverting everything. ... > We could settle on using "if/elsif" when there are multiple > conditions, and "or else" if there is only one, but I am not convinced > that makes sense. I do accept Randy's argument that redoing all of > the existing ones in the Containers would be a pain, and if we really > decide we want to do this someone else ought to volunteer to do the > shift over (e.g. me ;-). To be truly useful, you'd have to update the .MSS files that define the RM contents. If I have to do that, it doesn't save much (if any) effort. Note that I put the current definition directly in the .MSS files, it never existed anywhere else (outside of the AI samples that I showed the ARG before doing this). And I extracted the resulting specs for syntax checking directly from the text version of the RM. **************************************************************** From: John Barnes Sent: Friday, February 14, 2020 7:36 AM I have been glaring at some of these messages about pre/post conditions. I am both confused and very concerned that a lot of time could be wasted and errors introduced because of some fetish that lumps of Ada are easier to understand than existing bits of English. Is the basic problem that in Ada 2012 the only thing one can do with a precondition that fails is to get Assertion_Error? I found that in reviewing my book recently that I thought one could use Dynamic Predicate to force something else to happen. Obviously not so. But we do need to be able to do something else so I feel that adding or else plus an alternative statement does the job nicely. pre => precondition or else statement I find or else on its own perfectly acceptable. A brilliant idea. But anything more elaborate seems far too hard to read. The discussions don't seem to be coming to a conclusion. And we don't want to waste Randy's time going endlessly through the RM changing understandable English into confusing Ada text. And would that mean that if I rewrite my book (which I hope to do) I would have to add esoteric clutter everywhere to match the ARM text? Please not. **************************************************************** From: Erhard Ploedereder Sent: Monday, February 17, 2020 9:38 AM A few words about idiomatic use in this context ... With my students, I always insisted that they specify the preconditions and the reactions upon violation, be it in prose or in some (semi-)formalism. So, my idiomatic use follows the pattern precondition or else reaction for each simple precondition. If there are more preconditions, link them with "and". DO NOT bother to merge conditions merely because the reaction is the same. DO NOT bother with "and then", since the "or else" will, in 99% of all cases, raise an exception anyhow, so the short-circuiting is merely mental ballast without performance gain. NEVER omit the 'or else" (I want to know how violations are dealt with, i.e. which exceptions hops out). I don't see how confusion over logical formulas can arise, where the prose of the RM would not face the very same problem (and if it does, the prose better be fixed). That is the big advantage of formalizing. No room for interpretation, guessing, etc. and hence a great tool to achieve precision. But, of course, it leaves the same room for error. If the ARG goes for a model where the raising of exceptions is not (intended to be) part of the Ada precondition, then all the plentiful factual preconditions of library routines cannot be expressed as Ada PREs, because they would all end in Assertion_Error, prior to any possible differentiation by the code. Yes, this is a lot of specification work. but it is no harder (actually easier) than the hard-coding of the exceptional semantics that otherwise goes on in the body. A side-issue to deal with: suppression for Ada PREs suppresses the checks defined in the RM? **************************************************************** From: Tucker Taft Sent: Monday, February 17, 2020 11:11 AM > ... > A side-issue to deal with: suppression for Ada PREs suppresses the > checks defined in the RM? This is discussed in the section on Assertions and Assertion Policy, RM 11.4.2, paragraphs 23.4/5-23.e/5. Below is the entire Implementation Requirements" part of that section of the manual, which covers all kinds of assertion expressions that appear in the specification of language-defined units. The main point is that you can use pragma Suppress (with the usual erroneousness if they would have failed), as a way to turn off some of the precondition checking (though the implementation need not actually obey that). Assertion_Policy in any case has no effect on these language-defined assertion expressions. ---------- AARM 11.4.2 (23.2/5-23.e/5) --------- Implementation Requirements 23.2/5 {AI12-0179-1} {AI12-0265-1} Any postcondition expression, type invariant expression, or default initial condition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1, 7.3.2, and 7.3.3). 23.a/5 Ramification: The Assertion_Policy does not have an effect on such postconditions, invariants, and default initial conditions. This has no execution impact since such assertions shouldn't fail anyway (see the next rule). 23.3/5 {AI12-0179-1} {AI12-0265-1} The evaluation of any such postcondition, type invariant, or default initial condition expression shall either yield True or propagate an exception from a raise_expression that appears within the assertion expression. 23.b/5 Ramification: In other words, evaluating such an an assertion expression will not return a result of False, nor will it propagate an exception other than by evaluating a raise_expression which is syntactically all or part of the assertion expression. 23.c/5 To be honest: Evaluation of any expression might raise Storage_Error. 23.d/5 Reason: This allows the Standard to express semantic requirements as postconditions, invariants, or default initial conditions (which are invariably clearer than English prose would be) while keeping it clear that failing the assertion check (or any other run time check) is not conforming behavior. 23.4/5 {AI12-0112-1} Any precondition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1) unless suppressed (see 11.5). Similarly, any predicate checks for a subtype occurring in the specification of a language-defined unit are enabled (see 3.2.4) unless suppressed. 23.e/5 Reason: This allows the Standard to express runtime requirements on the client of a language-defined unit as preconditions or predicates (which are invariably clearer than English prose would be). Some such requirements can be Suppressed. Ada 2012 and earlier versions did not provide a mechanism to suppress such code. **************************************************************** From: Randy Brukardt Sent: Monday, February 17, 2020 6:55 PM > If there are more preconditions, link them with "and". > DO NOT bother to merge conditions merely because the reaction is the > same. DO NOT bother with "and then", since the "or else" will, in 99% > of all cases, raise an exception anyhow, so the short-circuiting is > merely mental ballast without performance gain. NEVER omit the 'or else" > (I want to know how violations are dealt with, i.e. which exceptions > hops out). A quibble here: short-circuiting serves to determine the order that the conditions are checked. Unless the conditions are all completely disjoint (which is rare), which "result" is chosen depends on the order the checks are made. If one uses "and", that order is up to the compiler, so what happens for any particular call would depend on the implementation and possibly even the contents of the precondition. [Not to mention that some programming style guides, including ours, uses short-circuits consistently -- I only use "and" or "or" in the very rare cases where both sides must be evaluated.] For instance, in the containers example I gave earlier, one has to use short circuits so the tampering check is made first, the null cursor check is made second, and the "wrong container" check is made third. Some other order would be wrong, in that all of three of these conditions could be true at once (and Has_Element is always true for a null cursor). > I don't see how confusion over logical formulas can arise, where the > prose of the RM would not face the very same problem (and if it does, > the prose better be fixed). That is the big advantage of formalizing. This is simplistic. Much of the prose in the RM is written in terms of identifying error conditions and the result of that error. For instance, "if Position is null, then ", or "A check is made that the prefix is not null, occurs if the check fails". I think a lot of prose in programs is the same; that's especially true as English really only allows one "otherwise" while programs tend to have many. Whereas a precondition is specifying non-error conditions, so it necessarily is the negative of the error condition. Both ways of specifying are complete in the same way, but the polarity is different. > No room for interpretation, guessing, etc. and hence a great tool to > achieve precision. But, of course, it leaves the same room for error. Maybe even more room for error if the polarity of the conditions is reversed in the precondition vs. the prose. I started using "or else" for the containers and switched to if-expressions because it more closely matched the prose. With all of the extra "not"s needed to match the prose in the "or else" form, I thought the chances of error were much higher (especially as one would try to eliminate the extra nots when possible). > If the ARG goes for a model where the raising of exceptions is not > (intended to be) part of the Ada precondition, then all the plentiful > factual preconditions of library routines cannot be expressed as Ada > PREs, because they would all end in Assertion_Error, prior to any > possible differentiation by the code. > > Yes, this is a lot of specification work. but it is no harder (actually > easier) than the hard-coding of the exceptional semantics that > otherwise goes on in the body. Absolutely. The issue is that the prose is very likely to be the inverse of the precondition (at least if one writes preconditions with "or else" rather than as if-expressions). > A side-issue to deal with: suppression for Ada PREs suppresses the > checks defined in the RM? Tucker covered this. Ada language-defined Preconditions are treated specially, since it is likely to be impractical to recompile language-defined units. (The Assertion_Policy for a unit is determined when it is compiled; it doesn't depend on the policy of the caller.) **************************************************************** From: Erhard Ploedereder Sent: Tuesday, February 18, 2020 5:18 AM > A quibble here: short-circuiting serves to determine the order that > the conditions are checked. Unless the conditions are all completely > disjoint (which is rare), which "result" is chosen depends on the > order the checks are made. If one uses "and", that order is up to the > compiler, so what happens for any particular call would depend on the > implementation and possibly even the contents of the precondition. I stand corrected. (So, I need to amend my guidance to include "and then" for ordered checks.) ****************************************************************