Login | Register
My pages Projects Community openCollabNet

Discussions > users > Ada.Containers and SPARK

Discussion topic

Back to topic list

Ada.Containers and SPARK


Author Matthew Heaney <mheaney at on2 dot com>
Full name Matthew Heaney <mheaney at on2 dot com>
Date 2005-11-28 13:21:33 PST
Message Geoff:

You asked here:


about Ada.Containers and SPARK.

Does SPARK support generics?

For sure it doesn't support dynamic allocation, so there'd have to be
some other way to handle that. Does SPARK support discriminants that
control the size of an array component, e.g.

type List (Capacity : Count_Type) is limited private;

then you could say

L : List (42);

and the list object would be declared with storage for up to 42 elements.

Another possibility is to say in the list package:

type Node_Array is array (Count_Type range <>) of Node_Type;
type List (Nodes : access Node_Array) is limited private;

and then at the point of declaration say:

N : aliased Node_Array (42);
L : List (N'Access);

but I don't know if SPARK does that either.

Yet another possibility is to declare the node array object in the
package body (so it would not have to be passed as a discriminant), and
then control the size of the node array via a generic formal constant, i.e.:

   type ET is ...;
   Capacity : in Count_Type;
package Ada.Containers.Doubl​y_Linked_Lists is ...;

Another other possibility is to simply #hide the entire body.


« Previous message in topic | 1 of 2 | Next message in topic »


Show all messages in topic

Ada.Containers and SPARK Matthew Heaney <mheaney at on2 dot com> Matthew Heaney <mheaney at on2 dot com> 2005-11-28 13:21:33 PST
     RE: Ada.Containers and SPARK SparkInfo <sparkinfo at praxis-his dot com> SparkInfo <sparkinfo at praxis-his dot com> 2005-11-29 00:28:31 PST
Messages per page: