Re: Assertions

[dale@cs.rmit.edu.au (Dale Stanbrough)]

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