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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,1e5c102037393131 X-Google-Attributes: gid103376,public From: "Nick Roberts" Subject: Re: Assertions Date: 1999/05/23 Message-ID: <37484098@eeyore.callnetuk.com> X-Deja-AN: 481230006 References: <3736D243.1EEBF1AB@globalnet.co.uk> <3736F549.E3DDCDEB@pwfl.com> <7h83lc$rd$1@nnrp1.deja.com> <3739CECA.6A49865B@averstar.com> <1999May12.163911.1@eisner.decus.org> <373c862b@eeyore.callnetuk.com> <3742eba5@eeyore.callnetuk.com> <7i7ei9$93v$1@nnrp1.deja.com> X-Original-NNTP-Posting-Host: da132d213.dialup.callnetuk.com X-Mimeole: Produced By Microsoft MimeOLE V4.72.3110.3 X-Complaints-To: newsabuse@remarq.com X-Trace: 927481890 02H499TBW8004D443C uk25.supernews.com Organization: RemarQ http://www.remarQ.com Newsgroups: comp.lang.ada Date: 1999-05-23T00:00:00+00:00 List-Id: Robert Dewar wrote in message <7i7ei9$93v$1@nnrp1.deja.com>... |In article , | Ray Blaak wrote: |> |> I would suggest the name "Verify" for assertions intended to |> be runtime checks, and "Assume" for assertions intended to |> give info to the compiler. | |In any case, this thread should have adequately demonstrated |that | |(a) this is quite a tricky subject |(b) it is not easy to propose a solution that gets any kind of | consensus agreement. | |This has always been the case when this issue has been |discussed, so it is hardly surprising to see it happening again |:-) Robert is absolutely right on both points, of course. However, I don't actually recall anybody actually suggesting anything to the contrary. I, for one, never expected otherwise. Of course it's a tricky subject! Of course consensus is not going to be handed to us on a plate! However, I would suggest that we can, nevertheless, attempt to negotiate this tricky subject, and to persue a sufficient consensus. If people hadn't taken this attitude towards almost all aspects of the development of the Ada standard, there would never have been an Ada language at all. At this point, I think I can suggest five possible pragmas as candidates for a future revision of the Ada standard (and perhaps for prior de facto adoption): ============================================================ pragma Assume (Condition); pragma Verify (Condition); The Assume and Verify pragmas are allowed anywhere a declaration or a statement is allowed. When the pragma would be elaborated, if it were a declaration, or executed, if it were a statement, the pragma is said to be executed. For execution of the Assume pragma, the compiler is allowed, but not required, to test the Condition, but in either case is allowed to assume that the Condition is true for the purposes of optimisation. For execution of the Verify pragma, the compiler is required, unless suppression of Verify_Check applies, to test the Condition is true. If the suppression of Verify_Check applies, the compiler is allowed, but not required, to omit this test. In any case, the compiler is allowed to assume that the Condition is true for the purposes of optimisation. pragma Verify_Before_Call (Subprogram,Condition); pragma Verify_Before_Return (Subprogram,Condition); These two pragmas are allowed anywhere a declaration is allowed in the public part of a package specification. The Subprogram must be the name of a subprogram declared before the pragma in the same specification. The condition may contain the names of any of the parameters of the subprogram, as well as any entity that would normally be visible at the point of the pragma (but not any entity in the body of the subprogram). The Verify_Before_Call pragma causes the execution, with the same Condition, of an implicit Verify pragma just before the first declaration, or, if the subprogram has no declarations, as the only declaration, of the subprogram. The Verify_Before_Return pragma causes the execution, with the same Condition, of an implicit Verify pragma just after the evaluation of the return expression of a return statement in the subprogram, or just before the execution of a return statement in the subprogram which has no return expression. For both these pragmas, the meanings of the names in the Condition shall be interpreted at the place of the pragmas (not at the places of their implicit execution). For all four of these pragmas, if the test of the Condition is actually done, and it fails (evaluates to False), the predefined exception Program_Error is raised. (If this exception is raised by a pragma which takes the place of a declaration, the exception is immediately propagated out the innermost enclosing block, and is never handled by an exception handler inside this block.) [There is a new check for the Suppress pragma, Verify_Check.] pragma Parallel_Loop [(Loop_Name)]; This pragma is allowed anywhere a statement is allowed, but must apply to loop. With no parameter, this pragma applies to the innermost enclosing loop statement; otherwise this pragma applies to loop whose name is Loop_Name. The loop must have an iteration scheme of the 'for' variety, and this iteration scheme must not include the reserved word 'reverse'. The pragma Parallel_Loop allows the compiler to assume, for the purposes of optimisation, that the loop it applies to has the following property: execution of the iterations of the loop may be arbitrarily overlapping, and in any order, without changing the effect of the loop. The compiler is allowed, but not required, to test that the loop actually has this property; if such a test is done, and fails, the predefined exception Program_Error is raised. ============================================================ It may well be better to use 'Assert' throughout rather than 'Verify'. Comments please. Does this count as a stoneman? :-) I hope no-one objects to my throwing in the last pragma, but it seemed reasonably appropriate. Sorry, I must go now, my mum is expecting her cup of tea ;-) ------------------------------------- Nick Roberts -------------------------------------