reviewing the list of source files

6-08-12
(I)

I reviewed the list of source files and I saw that practically the unique changed file is hi-lite/libs/containers/ada/DLL/a-cfdlli.ads 

the rest of file list are the same, that was distributed on the gnat gpl version. 

Original-file-list Hi-lite sources Rts-native Rts-sjlj

a-cbdlli.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cbdlli.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cbdlli.ads

a-cbhama.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cbhama.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cbhama.ads

a-cbhase.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cbhase.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cbhase.ads

a-cborma.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cborma.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cborma.ads

a-cborse.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cborse.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cborse.ads

a-cdlili.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cdlili.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cdlili.ads

a-cfdlli.ads /Altro/socis/hi-lite/libs/containers/ada/DLL/a-cfdlli.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cfdlli.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cfdlli.ads

a-cfhama.ads /Altro/socis/hi-lite/libs/containers/ada/HAMA/a-cfhama.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cfhama.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cfhama.ads

a-cfhase.ads /Altro/socis/hi-lite/libs/containers/ada/HASE/a-cfhase.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cfhase.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cfhase.ads

a-cforma.ads /Altro/socis/hi-lite/libs/containers/ada/ORMA/a-cforma.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cforma.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cforma.ads

a-cforse.ads /Altro/socis/hi-lite/libs/containers/ada/ORSE/a-cforse.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cforse.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cforse.ads

a-cidlli.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cidlli.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cidlli.ads

a-cihama.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cihama.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cihama.ads

a-cihase.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cihase.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cihase.ads

a-ciorma.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-ciorma.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-ciorma.ads

a-ciormu.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-ciormu.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-ciormu.ads

a-ciorse.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-ciorse.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-ciorse.ads

a-cobove.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cobove.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cobove.ads

a-cofove.ads /Altro/socis/hi-lite/libs/containers/ada/VE/a-cofove.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cofove.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cofove.ads

a-cohama.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cohama.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cohama.ads

a-cohase.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-cohase.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-cohase.ads

a-coinve.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coinve.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coinve.ads

a-convec.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-convec.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-convec.ads

a-coorma.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coorma.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coorma.ads

a-coormu.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coormu.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coormu.ads

a-coorse.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-coorse.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-coorse.ads

a-crdlli.ads

/usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-native/adainclude/a-crdlli.ads /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/rts-sjlj/adainclude/a-crdlli.ads

At first I want to ask you about  nomenclature, what does DLL, HAMA, HASE, ORMA, ORSE and VE mean?

Should I use the same source files? like a-cobove.ads to write new code for Replace_Element, this procedure is used in lists and Vectors

if I have to define new source files

Should I use the large  naming style (i.e., ada-containers-bounded_vectors.ads) or short style ((i.e., a-cobove.ads)?

To get you started

1-08-12
(Them)

To get you started, you'll need to get an account on Open-DO forge and join the project Hi-Lite:

- go to https://forge.open-do.org/ and create a new account

- when this is accepted, log in and ask to join project Hi-Lite on

  https://forge.open-do.org/projects/hi-lite/

- when this is accepted, clone the git repository:

  git clone --recursive git+ssh://developername@scm.forge.open-do.org//scmrepos/git/hi-lite/hi-lite.git

- note that you can upload your SSH key to avoid typing your password

  each time you access the remote repository (go to MyPage menu, then

  AccountMaitenance, then at the bottom EditKeys)

If you need help with git, don't hesitate to ask. You can also look at this book online: http://git-scm.com/book (chapter 2 is enough)

You should restrict your commits to the directory hi-lite/libs/containers/ada which already contains the version of formal containers developed by Claire Dross. If you've not done it yet, you should read the sections 1 and 2 of her paper "Correct Code Containing Containers" (http://www.open-do.org/wp-content/uploads/2011/06/Correct_Code_Containing_Containers.pdf) that explain what is different between these "formal" containers and the usual ones. I propose that you create a sub-directory inside hi-lite/libs/containers/ada for each family of formal containers on which you'll work.

3-08-12
(I)

I had already installed gtat gpl and gnat-coll

 gnatls -v

GNATLS GPL 2012 (20120509)

Copyright (C) 1997-2012, Free Software Foundation, Inc.

Source Search Path:

   <Current_Directory>

   /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/adainclude/

Object Search Path:

   <Current_Directory>

   /usr/gnat/lib/gcc/i686-pc-linux-gnu/4.5.4/adalib/

Project Search Path:

   <Current_Directory>

   /usr/gnat/i686-pc-linux-gnu/lib/gnat

   /usr/gnat/share/gpr

   /usr/gnat/lib/gnat

[panzon@baleada hi-lite]$ 

but I have a doubt cause in the hi-lite/build_instructions.txt (HI-LITE BUILD INSTRUCTIONS FOR ADACORE DEVELOPERS)

on  2.2) I had the same alt-ergo messages

git submodule init

[panzon@baleada hi-lite]$ git submodule update

fatal: Needed a single revision

Unable to find current revision in submodule path 'alt-ergo'

And then on  3) I don't gnat pro and also you didn't said me anything about Ocaml

So that made me think that maybe I'm doing wrong things

by the other hand, I already read the article and I searched some books on my university but we don't have anything about ada 2012, (perhaps no book has been published in 2012 http://en.wikibooks.org/wiki/Ada_Programming/Ada_2012)

The best book I could find was Programing in Ada 95, Jhon Barnes Addison Wesley

If you have a better reference please let me know.

I don't know what is the .gpr I had to use

or maybe I have to write a new one.

a proposed work breakdown for the internship

1-08-12

(Them)

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

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

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

Hashed sets:
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

Ordered sets:
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

Ordered multisets:
ada-containers-indefinite_ordered_multisets.ads -> a-ciormu.ads
ada-containers-ordered_multisets.ads -> a-coormu.ads

Hashed maps:
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

Ordered maps:
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:
    Replace_Element
    Insert
    Replace
    Delete
    Include
    Exclude
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:

   procedure Replace_Element
     (Container : in out Map;
      Position  : Cursor;
      New_Item  : Element_Type)
   with
     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.