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,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: dale@cs.rmit.edu.au (Dale Stanbrough)
Subject: Re: Assertions
Date: 1999/05/22
Message-ID: <dale-2205990829190001@r1021c-20.ppp.cs.rmit.edu.au>#1/1
X-Deja-AN: 480693078
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>
X-Complaints-To: abuse@cs.rmit.edu.au
X-Trace: emu.cs.rmit.edu.au 927325760 24196 131.170.66.220 (21 May 1999
 22:29:20 GMT)
Organization: RMIT
NNTP-Posting-Date: 21 May 1999 22:29:20 GMT
Newsgroups: comp.lang.ada
Date: 1999-05-21T22:29:20+00:00
List-Id: <comp.lang.ada>

Nick Roberts wrote:

" Could you give, please, one or two further examples, in a little more
  detail?  I (if no-one else!) would appreciate this."

in response to my statement...

  |I want some assertions to be genuinely tested, while others to be used
  |as an adjunct to the type system (and thus the compiler can use it for
  |optimisation purposes).


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.


For an assertion that could be used by the compiler to optimise
the code


   pragma Enforce (X in 1..9 or X in 20..29);

   case X is
      when  1..10 => Something;
      when 20..29 => Something_Else;
      when others => Put_Line ("Whoops!");
   end case;


In this example, the compiler could remove the others clause.
The "Enforce" (I don't think this is a good name, but I can't
think of anything better) is used to extend the type system.

One problem with the name "Assert" is that people have 
different views about what it actually means. Robert Dewar
considers that "Assert" _should_ be able to be used for
optimisation purposes.


Dale