Here is a proposed work breakdown for the internship:
0. Read the section of the Ada reference manual on containers (http://www.ada-auth.org/standards/12rm/html/RM-A-18.html). It can be useful also that you have a look at the implementation of the Ada standard container library in GNAT. You can get access to it in the GNAT GPL 2012 release (see libre.adacore.com to download it). After installation, just type 'gnatls -v' in a shell and it will give you the Search Path for the standard includes. Here is the complete list of units (the ads for spec, and there is course a corresponding adb for the body) for the standard Ada containers. On the left this is the name that you would expect, and on the right the actual name (due to some constraint on filenames in early DOS systems, all run-time library units have an 8-character name).
ada-containers-bounded_vectors.ads -> a-cobove.ads
ada-containers-formal_vectors.ads -> a-cofove.ads
ada-containers-indefinite_vectors.ads -> a-coinve.ads
ada-containers-vectors.ads -> a-convec.ads
ada-containers-bounded_doubly_linked_lists.ads -> a-cbdlli.ads
ada-containers-doubly_linked_lists.ads -> a-cdlili.ads
ada-containers-formal_doubly_linked_lists.ads -> a-cfdlli.ads
ada-containers-indefinite_doubly_linked_lists.ads -> a-cidlli.ads
ada-containers-restricted_doubly_linked_lists.ads -> a-crdlli.ads
ada-containers-bounded_hashed_sets.ads -> a-cbhase.ads
ada-containers-formal_hashed_sets.ads -> a-cfhase.ads
ada-containers-hashed_sets.ads -> a-cohase.ads
ada-containers-indefinite_hashed_sets.ads -> a-cihase.ads
ada-containers-bounded_ordered_sets.ads -> a-cborse.ads
ada-containers-formal_ordered_sets.ads -> a-cforse.ads
ada-containers-indefinite_ordered_sets.ads -> a-ciorse.ads
ada-containers-ordered_sets.ads -> a-coorse.ads
ada-containers-indefinite_ordered_multisets.ads -> a-ciormu.ads
ada-containers-ordered_multisets.ads -> a-coormu.ads
ada-containers-bounded_hashed_maps.ads -> a-cbhama.ads
ada-containers-formal_hashed_maps.ads -> a-cfhama.ads
ada-containers-hashed_maps.ads -> a-cohama.ads
ada-containers-indefinite_hashed_maps.ads -> a-cihama.ads
ada-containers-bounded_ordered_maps.ads -> a-cborma.ads
ada-containers-formal_ordered_maps.ads -> a-cforma.ads
ada-containers-indefinite_ordered_maps.ads -> a-ciorma.ads
ada-containers-ordered_maps.ads -> a-coorma.ads
1. Augment the existing formal containers with functions corresponding to the procedures:
The goal is to be able to say, for example, that in postcondition of the procedure Replace_Element, the input and output containers are related by the function Replace_Element:
(Container : in out Map;
Position : Cursor;
New_Item : Element_Type)
Post => Container = Replace_Element (Container'Old, Position, New_Item);
Of course, there is not much benefit here. The real benefit is when the user can use these functions on his own code to specify the behavior of some programs.
2. Add contracts (pre- and postconditions) to the Ada formal containers, based on the contracts written by Claire on the intermediate Why3 representation. You will have to look at the containers/why repository to see these existing contracts, and we'll probably need to discuss live before you start on this.
3. Develop a library of unbounded formal containers. Right now, the library developed by Claire is bounded: when defining a container, the user must declare a fixed maximal size, which is statically allocated, for example:
L : List(100); -- at most 100 elements in this list
We'd like to have another library that allows dynamically resizing the containers, like it is done in the standard Ada container library. Of course, this library will need to use dynamic allocation.
4. Develop a library of bounded and unbounded indefinite formal containers. That is, containers which can hold elements of an indefinite type (= unknown size). This is in particular the case for the classwide types like T'Class. So this library would make it possible to have containers of classwide objects on which the user could call dispatching subprograms. We'll need to discuss more before you start on that.