Ada 200X Assertions

Ada 200X Assertions

[Richard Riehle]

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

Richard Riehle
richard@adaworks.com
http://www.adaworks.com

Re: Ada 200X Assertions

[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; 
   

Re: Ada 200X Assertions

[Robert Dewar]

lutz@iks-jena.de (Lutz Donnerhacke) wrote in message news:<slrna0p3q9.n1.lutz@taranis.iks-jena.de>...
>    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.

A lot of people want some magic here, but in fact it is
very difficult to design a coherent language feature (i.e.
the step from the rough idea, which has been often
expressed, to a detailed proposal which holds water.

No one has achieved this yet. Someone needs to have something to
propose first. And is not good exhorting
others to work on this, they have and not solved the
problem. I personally don't think you can have a general
solution for many reasons, so the issue is simply whether
you can have a partial solution.

One thing we did in Realia COBOL was simply to have big and little
endian types (e.g. consider allowing bit order to
be specified for integer types). That's quite useful for
some of these cases, but magic is out :-)

>       type pascal_length is 0 .. 255;
>       type pascal_string(len : pascal_length) is record
>          data : String (1 .. len);
>       end record;

Well this is nonsense Ada, so let's try to first correct it
to something that compiles (I wish people would compile
code fragments before posting junk :-)

package z is
       type pascal_length is mod 2 ** 8;
       type pascal_chars is array (pascal_length range <>)         
                                            of character;   
       type pascal_string(len : pascal_length) is record
          data : pascal_chars (1 .. len);
       end record;
end z;                                      

Now the default representation of this in GNAT (and in
any reasonable compiler) is:

for pascal_string'Object_Size use 2048;
for pascal_string'Value_Size use  (((#1 max 0) * 8) + 8) ;
for pascal_string'Alignment use 1;
for pascal_string use record
   len  at 0 range  0 ..  7;
   data at 1 range  0 ..  ((#1 max 0) * 8)  - 1;
end record;

which is exactly what you want (this by the way is output
from the GNAT -gnatR3 switch, and #1 means the value of
the first discriminant.

Yes, it would be nice to have a way of specifying this
for sure, but it is hardly a critical problem in practice.

>       for pascal_string use record
>          len  at 0 range 0 .. 7;
> 	 data at 1 range 0 .. 8*len - 1;
>       end record;

This solution won't fly at all, it is has horrible
implications, since the situations in which expressions
of this kind could be used are very limited, and the list
of rules would be junk. For example, if you allow

            len at 0 range 7+len;

you have a huge mess on your hands.

So your solution here is the wrong solution to the problem.
I would guess it would be good enough to simply be able
to give the static starting position

perhaps something like

         data at 1 range 0 .. <>;

where the meaning of <> is that you will let the
compiler choose. 

> 
>    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.
>  
> 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;

Re: Ada 200X Assertions

[Matthew Heaney]

"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
news:slrna0p3q9.n1.lutz@taranis.iks-jena.de...
> * Richard Riehle wrote:
> 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:
[snip]
>    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.

What on Earth are you trying to do here?  Of course the language already
allows you to move from a pointer to component to a pointer to aggregate:
just use an access discriminant.

In the code below, List_Item behavior is "mixed in" with objects of type T,
allowing T objects to be inserted into List_Type objects.

All you need are access discriminants.  No Chapter 13 trickery is needed to
make this work.  It is completely safe.

Access discriminants are your friend.  If you're not using them, then you
haven't really groked the Ada95 way of doing things.


--STX
package body Lists is

   procedure Push
     (List : in out List_Type;
      Item : access List_Item_Type'Class) is
   begin
      Item.Next := List.Head;
      Item.Prev := null;
      List.Head := List_Item_Class_Access (Item);
   end;

   procedure Iterate (List : in out List_Type) is
      Item : List_Item_Class_Access := List.Head;
   begin
      while Item /= null loop
         Process (Item);
         Item := Item.Next;
      end loop;
   end;

end Lists;
package Lists is
   type List_Type is limited private;

   type List_Item_Type is abstract tagged limited private;
   type List_Item_Class_Access is access all List_Item_Type'Class;
   for List_Item_Class_Access'Storage_Size use 0;

   procedure Push
     (List : in out List_Type;
      Item : access List_Item_Type'Class);

   procedure Process (Item : access List_Item_Type) is abstract;

   procedure Iterate (List : in out List_Type);


private

   type List_Item_Type is abstract tagged limited record
      Next, Prev : List_Item_Class_Access;
   end record;

   type List_Type is limited record
      Head : List_Item_Class_Access;
   end record;

end Lists;

   with Ada.Text_IO; use Ada.Text_IO;

package body P is
   function List_Item (O : access T) return List_Item_Class_Access is
   begin
      return O.Item'Access;
   end;

   procedure Process (Item : access T_List_Item) is
   begin
      Put_Line ("processing T list item");
   end;
end P;
with Lists;  use Lists;

package P is
   type T is limited private;
   function List_Item (O : access T) return List_Item_Class_Access;
private
   type T_List_Item (O : access T) is new List_Item_Type with null record;
   procedure Process (Item : access T_List_Item);
   type T is limited record
      Item : aliased T_List_Item (T'Access);
   end record;
end P;
with Lists; use Lists;
with P;  use P;

procedure Test_Lists is

   O1 : aliased T;
   O2 : aliased T;

   L : List_Type;

begin

   Push (L, List_Item (O2'Access));
   Push (L, List_Item (O1'Access));

   Iterate (L);

end;

Re: Ada 200X Assertions

[Randy Brukardt]

Richard Riehle wrote in message <3C0C48BE.3B20F04E@adaworks.com>...
>Does anyone know whether there is still serious
>consideration for pre-, post-, and invariant assertions
>in the next version of ISO Standard Ada?

The ARG does not have any serious proposal for this on the table. There
is an action item for it, but that may or may not lead to anything.

To consider it, we need a serious (detailed) proposal, and probably a
champion within the ARG. My guess is that someone would come forward to
support a proposal if it was made.

                Randy Brukardt
                ARG Editor

Re: Ada 200X Assertions

[Ehud Lamm]

Randy Brukardt <randy@rrsoftware.com> wrote in message
news:9uj730$shr$1@news.online-isp.com...
> To consider it, we need a serious (detailed) proposal, and probably a
> champion within the ARG. My guess is that someone would come forward to
> support a proposal if it was made.


I am doing some research on DbC and Ada, following some interesting recently
published results.
If anyone is interested in details, let me know.

Ehud

Re: Ada 200X Assertions

[Volkert]

Richard Riehle <richard@adaworks.com> wrote in message news:<3C0C48BE.3B20F04E@adaworks.com>...
> Does anyone know whether there is still serious
> consideration for pre-, post-, and invariant assertions
> in the next version of ISO Standard Ada?

i like idea of extending Ada with Assertions too. 
The Design By Contract philosophie is one of the 
main reasons why we still teaching Eiffel in our
Programming Courses at the University. But before talking 
about an Ada language extension, i would like to see an 
Assertion-Precompiler for Ada similar to iContract 
in the Java World. With ASIS we have the right
technology, i think ...

With regards,
Volkert Barr

Re: Ada 200X Assertions

[Lutz Donnerhacke]

* Robert Dewar wrote:
>lutz@iks-jena.de (Lutz Donnerhacke) wrote in message news:<slrna0p3q9.n1.lutz@taranis.iks-jena.de>...
>>    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.
>
>A lot of people want some magic here, but in fact it is very difficult to
>design a coherent language feature (i.e. the step from the rough idea,
>which has been often expressed, to a detailed proposal which holds water.

So I'm not too far away from a 'required' feature. ;-)

>No one has achieved this yet. Someone needs to have something to propose
>first. And is not good exhorting others to work on this, they have and not
>solved the problem. I personally don't think you can have a general
>solution for many reasons, so the issue is simply whether you can have a
>partial solution.

That's the best starting point for a AdaYY feature. ;-)

>One thing we did in Realia COBOL was simply to have big and little endian
>types (e.g. consider allowing bit order to be specified for integer
>types). That's quite useful for some of these cases, but magic is out :-)

The compiler should be able to generate code with endinaess prefixes directly.
That's all. No magic.

>Now the default representation of this in GNAT (and in any reasonable
>compiler) is:
>
>for pascal_string'Object_Size use 2048;
>for pascal_string'Value_Size use  (((#1 max 0) * 8) + 8) ;
>for pascal_string'Alignment use 1;
>for pascal_string use record
>   len  at 0 range  0 ..  7;
>   data at 1 range  0 ..  ((#1 max 0) * 8)  - 1;
>end record;

Exactly this should be specifyable.

>Yes, it would be nice to have a way of specifying this
>for sure, but it is hardly a critical problem in practice.

Sometimes (i.e. IPV4 Header) it would solve a lot, because I'd could
use the record instrinct discriminiants directly:
  for ipv4 use record
    ...
    head_len at 0 range 0 .. 3;
    ...
    options at 40 range 0 .. (8 * (head_len - 5));
    payload at 8*head_len range 0 .. (8 * len);
  end record;

>This solution won't fly at all, it is has horrible implications, since the
>situations in which expressions of this kind could be used are very
>limited, and the list of rules would be junk. For example, if you allow
>
>            len at 0 range 7+len;
>
>you have a huge mess on your hands.

I do not see the mess.

>So your solution here is the wrong solution to the problem. I would guess
>it would be good enough to simply be able to give the static starting
>position perhaps something like
>
>         data at 1 range 0 .. <>;
>
>where the meaning of <> is that you will let the compiler choose.

Yep, if I can set a discriminant depend starting position.

Re: Ada 200X Assertions

[Lutz Donnerhacke]

* Matthew Heaney wrote:
>"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
>> Problem 1: Pointer of component => Pointer to aggregate
[...]
>>    Of course this Conversion may return a Pointer to an invalid aggregate.
>
>What on Earth are you trying to do here?

I've a list of degenerated compound instantiations for which only a single
component is relevant. More than this, this same fixed component is shared
by multiple compound instantiations.

Typical example 1: A common termination node of linked lists.
Typical example 2: A head node of a linked list contains a next pointer which
                   should be handled exactly as the next pointer of the real
		   list nodes, but no payload at all.

It would be fine to generate a pointer from this component to a 'virtual'
aggregate of the given type.

Example:
   struct node {
     ... data ...
     struct node * next;
   }
   struct head {
     struct node * next;
   }
   
   struct head h;
   h.next = &h - sizeof (node) + sizeof (head);

AdaYY should be able to represent such structures.

>Of course the language already allows you to move from a pointer to
>component to a pointer to aggregate: just use an access discriminant.

This generates a completely different structure.

>   procedure Iterate (List : in out List_Type) is
>      Item : List_Item_Class_Access := List.Head;
>   begin
>      while Item /= null loop
>         Process (Item);
>         Item := Item.Next;
>      end loop;
>   end;

and end in a different algorithm:

  procedure Iterate (List : in out List_Type) is
     Item : List_Item_Class_Access := List.Next;
  begin
     while Item /= Item.Next loop
        Process (Item);
        Item := Item.Next;
     end loop;
  end;

Re: Ada 200X Assertions

[Matthew Heaney]

"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
news:slrna0seip.kq.lutz@taranis.iks-jena.de...
> Typical example 2: A head node of a linked list contains a next pointer
which
>                    should be handled exactly as the next pointer of the
real
>    list nodes, but no payload at all.

In the code below, I do this by making the List_Type a private derivation of
a Node_Type. Which means a List_Type, containing only the head pointer, can
be used exactly like Node_Type.

    type Node_Type is abstract tagged private;
    type List_Type is Node_Type;
private
   type Node_Type is abstract tagged record
      Next : Node_Class_Access;
   end record;
   type List_Type is new Node_Type with null record;


Of course, you could choose to make the List_Type is public derivation of
Node_Type.

   type Node_Type is abstract tagged private;
   type List_Type is new Node_Type with private;

How is this not adequate?


> >Of course the language already allows you to move from a pointer to
> >component to a pointer to aggregate: just use an access discriminant.
>
> This generates a completely different structure.

What's wrong with that?


--STX
package body Lists is

   procedure Process (Item : access Node_Type) is
   begin
      null;
   end;

   function Head (List : List_Type) return Node_Class_Access is
   begin
      return List.Next;
   end;

   function Cons (Item : Node_Type'Class) return List_Type is
      Node : constant Node_Class_Access := new Node_Type'Class'(Item);
   begin
      return List_Type'(Next => Node);
   end;

   function "&" (Item : Node_Type'Class;
                 List : List_Type) return List_Type is

      Node : constant Node_Class_Access := new Node_Type'Class'(Item);
      New_List : List_Type;
   begin
      Node.Next := List.Next;
      New_List.Next := Node;
      return New_List;
   end;

   procedure Iterate (List : in out List_Type) is
      Item : Node_Class_Access := List.Next;
   begin
      while Item /= null loop
         Process (Item);
         Item := Item.Next;
      end loop;
   end Iterate;

end Lists;
package Lists is

   type List_Type is private;

   type Node_Type is abstract tagged private;
   type Node_Class_Access is access all Node_Type'Class;

   procedure Process (Item : access Node_Type);

   function Head (List : List_Type) return Node_Class_Access;

   function Cons (Item : Node_Type'Class) return List_Type;

   function "&" (Item : Node_Type'Class;
                 List : List_Type) return List_Type;

   procedure Iterate (List : in out List_Type);

private

   type Node_Type is abstract tagged record
      Next : Node_Class_Access;
   end record;

   type List_Type is new Node_Type with null record;

end Lists;
with Ada.Text_IO;  use Ada.Text_IO;

package body P is

   procedure Process (O : access T) is
   begin
      Put_Line ("processing T object");
   end;

end P;with Lists;  use Lists;

package P is

   type T is new Node_Type with null record;

   procedure Process (O : access T);

end P;
with Lists; use Lists;
with P;  use P;
with Ada.Text_IO;  use Ada.Text_IO;

procedure Test_Lists is

   O1 : T;
   O2 : T;

   L : List_Type := Cons (O1);

begin

   Put_Line ("first iterate");
   Iterate (L);

   New_Line;

   L := O2 & L;

   Put_Line ("second iterate");

   Iterate (L);

end Test_Lists;

Re: Ada 200X Assertions

[Matthew Heaney]

"Matthew Heaney" <mheaney@on2.com> wrote in message
news:u0sq9mg90ecr7b@corp.supernews.com...
> In the code below, I do this by making the List_Type a private derivation
of
> a Node_Type. Which means a List_Type, containing only the head pointer,
can
> be used exactly like Node_Type.
>
>     type Node_Type is abstract tagged private;
>     type List_Type is Node_Type;

Oops.  I should have said
    type List_Type is private;

The actual code I provided is correct.

Re: Ada 200X Assertions

[Lutz Donnerhacke]

* Matthew Heaney wrote:
>"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
>> Typical example 2: A head node of a linked list contains a next pointer
>>     which should be handled exactly as the next pointer of the real
>>     list nodes, but no payload at all.
>
>In the code below, I do this by making the List_Type a private derivation of
>a Node_Type. Which means a List_Type, containing only the head pointer, can
>be used exactly like Node_Type.

>   type Node_Type is abstract tagged private;
>   type List_Type is new Node_Type with private;

That's not a generic mixin.

My job is:
  task type Bla is ...;
  type Blas is array (Positive range <>) of Bla;
  type Foo (len : Natural) is abstract record
    t : Bla (Positive'First .. len);
  end record;
  procedure Process (a : Foo) is abstract;
  
  package Bla_List is new List (Bla);
  package Bla_List2 is new List (Bla);

In short: I'm looking for a extension of existing types to well known data
structures.

>> >Of course the language already allows you to move from a pointer to
>> >component to a pointer to aggregate: just use an access discriminant.
>>
>> This generates a completely different structure.
>
>What's wrong with that?

The memory layout shared by some hardware.

Thanx for your non generic examples.

Access discriminants (was Re: Ada 200X Assertions)

[Mark Lundquist]

Hi Lutz,

"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
news:slrna0seip.kq.lutz@taranis.iks-jena.de...
> * Matthew Heaney wrote:
> >"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
> >> Problem 1: Pointer of component => Pointer to aggregate
> [...]
> >>    Of course this Conversion may return a Pointer to an invalid
aggregate.
> >
> >What on Earth are you trying to do here?
>
> I've a list of degenerated compound instantiations for which only a single
> component is relevant. More than this, this same fixed component is shared
> by multiple compound instantiations.
>
> Typical example 1: A common termination node of linked lists.
> Typical example 2: A head node of a linked list contains a next pointer
which
>                    should be handled exactly as the next pointer of the
real
>    list nodes, but no payload at all.

Matt is right -- access discriminants are the solution to your problem.  I
didn't read his example -- maybe he didn't address your specific example, or
maybe he did.  Anyway, I know just the problem you're talking about, and
this is the solution I came up with for my generic linked lists with header
nodes.  Access discriminants are the way for a component to provide a view
of an enclosing record, regardless of the name used to access the component.
Ada already has the exact feature you are asking for, all you need is the
vocabulary to "say it in Ada".

Here's an example for a singly-linked list.  Start with something like this:

 type Root_Link;
 type Root_Link_Access is access all Root_Link'Class;
 type Root_Link is tagged limited record
  Next : Root_Link_Access;
 end record;

That's your "degenerate" case, containing only the "relevant" component :-).
It has to be limited so that its descendants can be limited and thereby be
allowed access discriminants.   Note that the pointer type is declared as an
access-to-classwide; that's very important, it allows a link to point either
to the header node or to a "real" node.  Continuing on...

 type Node;

 type Node_Link (Self : access Node) is
  new Root_Link with null record;

 type Node is record
  Data : Data_Type;        -- Whatever
  Linkage : Node_Link (Self => Node'Access);    -- access discriminant now
denotes enclosing Node
 end record;

 type List is record
  Header : Root_Link;
 end record;

 subtype Iterator is Root_Link_Access;

Bingo!  A linked list with a degenerate header.  Now you can write something
like this (e.g. in your list package body):

 function Value (Here : Iterator) return Data_Type is
  pragma Suppress (Tag_Check);
  Linkage : Node_Link renames Node_Link (Here.All);    -- a "narrowing"
conversion ("downcast")
 begin
  return Linkage.Self.Data;
 end Value;

>
> It would be fine to generate a pointer from this component to a 'virtual'
> aggregate of the given type.

Yes, the "virtual" thing is the classwide type Root_Link'Class.

BTW, the term "aggregate" has a specific meaning in Ada and this is not it
:-)  You should use the Ada term, "record".

>
> Example:
>    struct node {
>      ... data ...
>      struct node * next;
>    }
>    struct head {
>      struct node * next;
>    }
>
>    struct head h;
>    h.next = &h - sizeof (node) + sizeof (head);
>

The Ada way is a lot nicer, isn't it.

This also illustrates how it is possible for a non-tagged type to have
inheritance.  In this case, your (non-tagged) Node type inherits the
property of "singly-linkedness".  This might not seem like that big of a
deal -- you might ask, why not just inherit directly using a derived
(tagged) type?  Answer: this is very cool in generics, where we don't want
to have to insist that the user's base type be tagged (by declaring our
formal type tagged).

Cheers,
Mark

Re: Ada 200X Assertions

[Matthew Heaney]

"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
news:slrna0seip.kq.lutz@taranis.iks-jena.de...
> I've a list of degenerated compound instantiations for which only a single
> component is relevant. More than this, this same fixed component is shared
> by multiple compound instantiations.

Can you use child generics?

generic
   <whatever>
package GP is
   <foo>
end GP;

generic
   <whatever>
package GP.C_G is
   <bar>
end GP.C_G;

Instantiate the root package:

package P is new GP (<whatever>);

which can now be shared among the child instantiations:

with GP.C_G;
package P.C1 is new P.C_G (<whatever>);

with GP.C_G;
package P.C2 is new P.C_G (<whatever>);

Is this adequate?  What about package parameters?

generic
   with package P is new GP (<>);
package GQ is
   <blah>
end GG;

package P is new GP (<whatever>);

package Q1 is new GQ (P);
package Q2 is new GQ (P);

Will this do the job?

I still don't understand your problem.

Re: Ada 200X Assertions

[Lutz Donnerhacke]

* Matthew Heaney wrote:
>"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
>> I've a list of degenerated compound instantiations for which only a single
>> component is relevant. More than this, this same fixed component is shared
>> by multiple compound instantiations.
>
>Can you use child generics?

Yes. It might solve the problem. I'll try several of the ideas in this
thread. Very interesting discussion, BTW. Thank you.

Re: Ada 200X Assertions

[Mark Lundquist]

"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
news:slrna0stp1.pjb.lutz@belenus.iks-jena.de...
> * Matthew Heaney wrote:
> >"Lutz Donnerhacke" <lutz@iks-jena.de> wrote in message
> >> Typical example 2: A head node of a linked list contains a next pointer
> >>     which should be handled exactly as the next pointer of the real
> >>     list nodes, but no payload at all.
> >
> >In the code below, I do this by making the List_Type a private derivation
of
> >a Node_Type. Which means a List_Type, containing only the head pointer,
can
> >be used exactly like Node_Type.
>
> >   type Node_Type is abstract tagged private;
> >   type List_Type is new Node_Type with private;
>
> That's not a generic mixin.
>
> My job is:
>   task type Bla is ...;
>   type Blas is array (Positive range <>) of Bla;
>   type Foo (len : Natural) is abstract record
>     t : Bla (Positive'First .. len);
>   end record;
>   procedure Process (a : Foo) is abstract;
>
>   package Bla_List is new List (Bla);
>   package Bla_List2 is new List (Bla);

Well, what you have there is not really a mixin, either.  That's just a
"plain old" generic list :-) (POGL).

The mixin idiom takes a generic formal tagged type, and exports an extension
of that type with additional properties/behaviors.

The POGL gives you an "externally-linked"/"containing"/"value-oriented"
list, where the collection owns the items.  The mixin gives you an
"internally-linked"/"by reference"/"object-oriented" list, where the client
owns the items.

Now... I'll bet you can take the example I wrote, or the one Matt wrote, and
figure out how to make either a generic mixin, or a plain old generic list,
with a header using the access discriminant technique.

Your example is of a list of tasks.  Since these are limited, you have two
ways to go:

1) Use a POGL (as shown in your example).  That POGL will have to have the
formal item type as limited; such a POGL does not do any assignments to the
items, even though it owns and creates them.  Instead, it returns pointers
to the items.

2) Use a mixin on a tagged container type, like this:

    type Bla_Container is tagged record
        Contents : Bla;
    end record;

    package Bla_Lists is new Lists_Mixin (Base => Bla);
    subtype Listable_Bla is Bla_Lists.Item_Type;                -- whatever


Best,
Mark

Re: Ada 200X Assertions

[Matthew Heaney]

"Mark Lundquist" <mlundquist2@attbi.com> wrote in message
news:NNwP7.2247$dp6.159279@rwcrnsc54...
> The mixin idiom takes a generic formal tagged type, and exports an
extension
> of that type with additional properties/behaviors.

Well, you could argue there are two mixin idioms: the one you describe here,
and another using access discriminants.

If it's not clear to CLA readers, here are the two techniques:

I. Generic Mixin

generic
   type Parent_Type (<>) is abstract tagged limited private;
package T_Mixin is
   type T is new Parent_Type with private;
   procedure Mixin_Op (O : in out T);
private
   type T is new Parent_Type with <whatever>;
end;

Now you can add T_Mixin behavior to an existing tagged type:

package P is
   type T is tagged limited private;
...
end P;

package Q is new T_Mixin (P.T);

Now you use Q.T wherever type T_Mixin.T is expected:

declare
   O : Q.T;
begin
   Mixin_Op (O);
end;

However, I almost never do this.  I prefer to use the access discriminant
approach.

II. Access discriminants

package T_Mixin is
   type T is abstract tagged limited private;
   type T_Class_Access is access all T'Class;
   procedure Mixin_Op (O : access T) is abstract;
private
   type T is abstract tagged limited null record;
end;

package P is
   type T is tagged limited private;
...
end P;

package Q is
   type NT is new P.T with private;
   function Mixin (O : access NT) return T_Mixin.T_Class_Access;
private
   type Q_Mixin (O : access NT) is new T_Mixin.T with null record;
   procedure Mixin_Op (O : access Q_Mixin);
   type NT is new T with record
      Mixin : aliased Q_Mixin (NT'Access);
   end record;
end Q;

Now you can use Q.NT wherever type T_Mixin.T is expected:

declare
   O : aliased Q.NT;
begin
   Mixin_Op (Mixin (O'Access));
end;

I've shown here what is essentially an Java-style interface.  It doesn't
have to be as ornate as this.  Most of the time all you need is a way to
mixin behavior into an existing type hierarchy.  The most common reason for
this is to add Controlled-ness to a type:

package P is
   type T is tagged limited private;
...
end P;

package P.C is
   type NT is new T with private;
private
   type Control_Type (O : access NT) is
     new Ada.Finalization.Limited_Controlled with null record;
   procedure Finalization (Control : in out Control_Type);
   type NT is new T with record
     Control : Control_Type (NT'Access);
   end record;
end P.C;

The type NT is a member of T'Class, but has "mixed in" Controlled behavior.
Type T itself has nothing to do with type Controlled.

The availability of this technique is the reason why Ada95 doesn't need
multiple inheritance.

Re: Ada 200X Assertions

[Richard Riehle]

Ehud Lamm wrote:

> Randy Brukardt <randy@rrsoftware.com> wrote in message
> news:9uj730$shr$1@news.online-isp.com...
> > To consider it, we need a serious (detailed) proposal, and probably a
> > champion within the ARG. My guess is that someone would come forward to
> > support a proposal if it was made.
>
> I am doing some research on DbC and Ada, following some interesting recently
> published results.
> If anyone is interested in details, let me know.
>
> Ehud

I just received, and am half-way through the reading of, "Design By Contract By
Example,"
by Dr. Richard Mitchell and Dr. Jim McKim.   Good book from Addison-Wesley.
Mitchell
and McKim are both long-time practitioners of DBC and they present the material
in an
entertaining and coherent way.    Most of the examples are in Eiffel since there
are few
alternative languages with direct support for DBC.   That being said, I think
Ada
practitioners can benefit from many of the ideas in the book.   I am enjoying
it.

Professor Dewar is correct when he says that it is easier to propose and problem
for
someone else to solve than to present an actual solution.   It sounds as if Dr.
Lamm is
taking on the job of seeking solutions for DBC within Ada.   Kudos to him.
Also,
I appreciate the quick feedback from Randy.    It is important to realize that
the idea
is on the table but still needs a lot of work, along with a champion.

Richard Riehle

Mixins (was Re: Ada 200X Assertions)

[Mark Lundquist]

"Matthew Heaney" <mheaney@on2.com> wrote in message
news:u0t8rui7mdo870@corp.supernews.com...
>
> Well, you could argue there are two mixin idioms: the one you describe
here,
> and another using access discriminants.
>

Interesting thought...

Your 2nd example is the classic "multiple views" idiom.   I had never
thought of calling it a "mixin" before (and Lutz had asked specifically
about generic mixins), but a mixin isn't a bad way of thinking of it.  My
linked-list example is a special case of this, because you normally wouldn't
override the operations of the mixed-in type -- Root_Link or whatever I
called it -- you'd just use it as is, without specialization.  In that way
it's more "mixin-like" than the general case of multiple views.

Now that you've got me thinking of this as a mixin, I may start calling it a
"composition mixin" idiom (to distinguish it from the generic mixin).

Taking the linked list example as I wrote it, it's also trivial to
"genericize" that code and make a generic mixin out of it.  That'll work
with anything that doesn't have unknown discriminants (the formal type for
the "base" type of the mixin can't be indefinite since it is a component of
the list element type).

-- mark

Re: Ada 200X Assertions

[Rod Chapman]

Richard Riehle <richard@adaworks.com> wrote in message news:<3C0EEC25.E2738366@adaworks.com>...

> It sounds as if Dr. Lamm is
> taking on the job of seeking solutions for DBC within Ada.   Kudos to him.

I hope any such effort starts with a good look at how SPARK works,
where support for DBC is very strong.  Even without explicit pre-
or post-conditions, a simple subprogram declaration in SPARK carries
a far more onerous contract than the same piece of text in Ada.

One critical issue is visibility - most non-trivial assertions involve
states which aren't visible according to Ada's rules, so we have
to have the "--# global" annotation to extend visibilty of state
in annotation context.  The design of a useful assertion mechanism
in Ada0Y or later would have to consider this need carefully.
 - Rod

Re: Ada 200X Assertions

[Mark Lundquist]

"Ehud Lamm" <mslamm@mscc.huji.ac.il> wrote in message
news:9ujf1c$hhr$1@news.huji.ac.il...
>
> I am doing some research on DbC and Ada, following some interesting
recently
> published results.
> If anyone is interested in details, let me know.

Very interested.

-- Mark

Re: Ada 200X Assertions

[David Thompson]

Lutz Donnerhacke <lutz@iks-jena.de> wrote :
...
> Typical example 1: A common termination node of linked lists.
> Typical example 2: A head node of a linked list contains a next pointer which
>                    should be handled exactly as the next pointer of the real
>    list nodes, but no payload at all.
>
> It would be fine to generate a pointer from this component to a 'virtual'
> aggregate of the given type.
>
("Virtual" in the sense that it is a struct/record that isn't stored,
but the link field within it would overlay the head link or whatever.)

> Example:
>    struct node {
>      ... data ...
>      struct node * next;
>    }
>    struct head {
>      struct node * next;
>    }
>
>    struct head h;
>    h.next = &h - sizeof (node) + sizeof (head);
>
This is quite wrong for C, or C++; pointer arithmetic works in units
of the size of the type pointed to (and the conversion cannot be
implicit).  Assuming you meant:
  h.next = (struct node *) ( (char*)&h
    + sizeof(struct head) - sizeof(struct node) );
  /* 'struct' can be omitted in C++,
    or in C if you also typedef struct x ... x */
or, equivalent and arguably more elegant:
  h.next = (struct node *)(&h + 1/*head*/) - 1/*node*/;

1) this isn't portable -- neither the C nor C++ standard
defines/guarantees computing pointers outside (before)
an object, except that you can compute (but not dereference)
a pointer "to" the end of an array or past a non-array object
to support idioms like:
  char x[10] = "foo", * p;
  for( p = x; p < &x[10] /* or x+10 */; p++ ) *p = 'x';

Even computing, much less using, your "virtual" pointer
is Undefined Behavior, meaning the implementation is
not required to check/catch/diagnose it or even work at all.

2) even on mainstream platforms where (C or C++) pointers
are just numbers, and subtracting and adding back an offset
does work reliably, that may be the wrong offset if struct node
is more strictly aligned than struct head, which is quite possible.
_This_ problem you can portably fix with:
  h.next = (struct node *) ( (char*)&h - offsetof(struct node,next) );
which also works for link fields not at the "end" of the structure,
and is a more direct representation of what you are doing to boot.

I would expect that on any system where this works for C/C++
the Ada equivalent with 'Address and 'Position works as well.

--
- David.Thompson 1 now at worldnet.att.net

Re: Ada 200X Assertions

[Lutz Donnerhacke]

* David Thompson wrote:
>I would expect that on any system where this works for C/C++
>the Ada equivalent with 'Address and 'Position works as well.

S.C'Position ist the attribute I was looking for. Thanx.