Login | Register
My pages Projects Community openCollabNet

Discussions > users > Ada.Containers and SPARK

charles
Discussion topic

Back to topic list

Ada.Containers and SPARK

Reply

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:

http://troop245.org/​ada/page/projects.ht​m

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

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


-Matt

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

Messages

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: