Re: Ada 200X Assertions

[lutz@iks-jena.de (Lutz Donnerhacke)]

* Richard Riehle wrote:
>Does anyone know whether there is still serious
>consideration for pre-, post-, and invariant assertions
>in the next version of ISO Standard Ada?

I'd like to go further and request Anna.

And like to append an old article on this subject:
\f
I have three sad problems (and a bonus problem) from my current projects.
If they can fixed by a compiler it would be very fine:

Problem 1: Pointer of component => Pointer to aggregate

  In order to mixin a generic list with head nodes not mixed into any other
  user defined structure I'd need to link not the base data but the mixin
  itself. Doing so I need to regenerate the whole aggregate pointer from
  a pointer of a component. Current (not tested) implementation:
  
with System.Address_To_Access_Conversions;

generic
   type Base is tagged limited private;
   type Mixin is tagged limited private;
package Unchecked_Upconversion is
   type Mixed is new Base with record
      mix : aliased Mixin;
   end record;
   
   package Mixin_P is new System.Address_To_Access_Conversions (Mixin);
   package Mixed_P is new System.Address_To_Access_Conversions (Mixed);
   
   Call_To_Mix_First : exception;
   function To_Base (mix : Mixin_P.Object_Pointer)
     return Mixed_P.Object_Pointer;
   function To_Mix (mixed : Mixed_P.Object_Pointer)
     return Mixin_P.Object_Pointer;
end Unchecked_Upconversion;

with System.Storage_Elements;
use System, System.Storage_Elements;

package body Unchecked_Upconversion is
   offset_found : Boolean := False;
   offset : Storage_Offset;
   
   use Mixed_P, Mixin_P;
   
   function To_Base (mix : Mixin_P.Object_Pointer)
     return Mixed_P.Object_Pointer is
   begin
      if not offset_found then
         raise Call_To_Mix_First;
      end if;
      return To_Pointer (To_Address (mix) - offset);
   end To_Base;
   
   function To_Mix (mixed : Mixed_P.Object_Pointer)
     return Mixin_P.Object_Pointer is
   begin
      if not offset_found then
	 offset := To_Address(mixed) -
	           To_Address(mixed.mix'Access);
         offset_found := true;
      end if;
      return mixed.mix'Access;
   end To_Mix;      
end Unchecked_Upconversion;

   It's clearly a workaround to fix a missing language feature. Even other
   solutions (i.e. using Base'Size) are only workarounds which may fail in
   complex situations (pragma Pack) even more likely.
   
   Of course this Conversion may return a Pointer to an invalid aggregate.
\f
Problem 2: Defining Byte_Order of record representations

   My low level networking application has to deal with low and big endian
   values on the net I want to handle with record representations clauses
   in order to get the benefits of compiler generated I/O functions.
   
   Unfortunly only the numeration of bits in the data may be specified.
   Values crossing a Storage_Element boundery can not be handled portably.
   Even worse Storage_Element'Size might not be a multiple of eight. So it's
   impossible to write portable programs.
   
   At the moment I use constructs like the following (introducing new error
   sources, because they are likely forgotten and a lot of legacy code):
      for xxx use (
         addr1 at 0 range 0 .. 7;
         addr2 at 1 range 0 .. 7;
      );
      ...
      addr : Address_Type := Unchecked_Conversion_To_Address (
                               to_uint16(x.addr1, x.addr2));
      if not addr'Valid then ...
      case addr is ...

      function to_uint16(low, high : uint8) return uint16 is
      begin
         if System.Default_Bit_Order = System.Low_Order_First then
	    return Unchecked_Conversion_To_U16 ((low, high));
	 else
	    return Unchecked_Conversion_To_U16 ((high, low));
	 end if;
      end to_uint16;
    
   I'd like to see a additional Byte_Order type and attribute to specify the
   most common byte orders indepenent from the used bit order. This attribute
   must include the conversions above in order to generate better code.
   Several CPUs does have a maschine language prefix to specify the byte and
   the bit order (in)depenty, It's only a bunch of hard wired gatters on the
   chip which should be usable from AdaYY.
\f
Problem 3: Static expressions of discriminants in record representations

   Trying to may a simple data structure like a Pascal string is not possible
   with Ada95. This is even worse in enviroments where memory mapped I/O
   contains such structures and must be handled using Atomic and Volatile
   Pragmas.
   
   It would be fine to use the following:
      type pascal_length is 0 .. 255;
      type pascal_string(len : pascal_length) is record
         data : String (1 .. len);
      end record;
      for pascal_string use record
         len  at 0 range 0 .. 7;
	 data at 1 range 0 .. 8*len - 1;
      end record;

   Additional suggestions are:
      - limit the restriction to specify discriminats at the very beginning.
        (currently possible)
      - limit the restriction to specify discriminats at statically known
        positions. Allow discriminant dependant discriminant positions.
      - limit the restriction of cycle free position specifications.
      - extend this concept to tagged records.
\f
Problem 4: Single task packages

   Several algorithms require hard work to deal with multitasking. Most of
   those algorithms consist of small and short running functions and
   procedures. On many CPUs those calls can be implemented very efficently
   using self modifying code. In order to generate such code the compiler
   has to determine which parts are single task and which might be
   interrupted. In order to ease this allow the following syntactic shugar
   constructs:
       protected package xxx ...
       protected procedure xxx ...
       protected function xxx ...
   which are similar but stronger than:
       proteced type yyy is
          procedure xxx;
       end yyy;
       y : constant yyy;   -- Singleton
       procedurce xxx is begin y.xxx; end xxx;