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.3 required=5.0 tests=BAYES_00,FREEMAIL_FROM,
	INVALID_MSGID autolearn=no 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" <nickroberts@callnetuk.com>
Subject: Re: Assertions
Date: 1999/05/23
Message-ID: <37482537@eeyore.callnetuk.com>#1/1
X-Deja-AN: 481203715
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>
 <dale-1705991202350001@dale.bu.cs.rmit.edu.au>
 <3742eba5@eeyore.callnetuk.com>
 <dale-2205990829190001@r1021c-20.ppp.cs.rmit.edu.au>
X-Original-NNTP-Posting-Host: da134d11.dialup.callnetuk.com
X-Mimeole: Produced By Microsoft MimeOLE V4.72.3110.3
X-Complaints-To: newsabuse@remarq.com
X-Trace: 927476250 02H499TBW8004D443C uk25.supernews.com
Organization: RemarQ http://www.remarQ.com
Newsgroups: comp.lang.ada
Date: 1999-05-23T00:00:00+00:00
List-Id: <comp.lang.ada>

Dale Stanbrough wrote ...
[...]
|For an assertion that I would like tested...
|
|   procedure Insert (Root : in out Tree; Item : Element) is
|   --  insert into a binary search tree
|   begin
|      -- insertion code.
|      ...
|
|      pragma Assert (Balanced (Root));
|          -- test this, die if it fails
|
|   end Insert;
|
|This assertion would cause an exception if the assertion failed
|(i.e. the semantics that Tucker Taft recently described). The
|compiler would not take advantage of this assertion to make any
|optimisations.


Supposing we had, at some other point in your code:

   Order_Pudding(Cherry_Pie);
   Insert(Cocktail,Umbrella);
   if not Balanced(Cocktail) then
      Have_Another(Cherry_Pie);
   end if;

[I'm also going to assume the program has no tasks (other than the main
task), and no volatile objects.]

The compiler could decide, at compile time, to forego the second serving of
pudding at this point.  It would still have to call Balanced; but only once,
as part of the assertion inside the body of Insert.

Of course, if suppression of assertions is allowed inside the body of
Insert, AND the compiler decides to comply with this suppression, then the
condition in the if...then here would have to be tested (and two cherry pies
are a theoretical possibility).  [Assuming the waiter is never clumsy (and
always balances the cocktail after inserting an umbrella into it), the
second pie will never happen, in practice, but the compiler probably can't
know this.]

I do not see how this kind of optimisation---based on an assertion---could
ever be a problem.  (Am I wrong?)

-------------------------------------
Nick Roberts
-------------------------------------

PS: I would like to take the opportunity here to thank the people who
responded to my questions in this thread.  I have found the discussion
illuminating and stimulating.