####################################################################
Minutes of the Vecolib Meeting
November 21, 2014 @ LIAFA
####################################################################

===================================================================
November 21st 2014, LIAFA
===================================================================

-------------------------------------------------------------------
Task 4: Tools and case studies
-------------------------------------------------------------------

'''''''''''''''''''''''''''''
Y. Moy presented the containers of Ada and SPARK
'''''''''''''''''''''''''''''

There are three kinds of containers that could be considered 
for this project: Ada 2000, Ada 2012, and SPARK containers.

***Ada 2005*** provides 6 kinds of containers parameterized 
by the signature of the data stored (see [Ada2005:Containers]):

.List 
.Vectors
.Map
.Set

The implementation is based on linked data structures and it was 
very inefficient because of per object allocation. 


[Ada2005:Containers] http://www.adacore.com/uploads/technical-papers/Ada05_rational_07.pdf



***Ada 2012*** provides 6 kinds of containers parameterized
by the signature of the data stored (see [Ada2012:Containers]):

.Vectors
.Doubly_Linked_Lists
.Hashed_Maps
.Ordered_Maps
.Hashed_Sets
.Ordered_Sets

To the old implementation (Ordered_*) has been added a new implementation
based on "closed addressing" hash tables, i.e., arrays of objects where
some fields are used to implement the list, tree, etc.
For the Map and Sets, red-black trees are encoded in these arrays.
This new implementation targets the embedded-critical market.
Notice that for both implementations, cursors (iterators) are pointers.
Also, callback mechanism for methods is not allowed.

[Ada2012:Containers] http://www.adacore.com/uploads/technical-papers/Ada2012_Rationale_Chp6a_containers-cc.pdf



***SPARK*** is the version of Ada 2012 used for programming critical software
which need to be fully proved.
SPARK provides "formal containers" which are the set of "hashed" 
version of containers with a slight change in the API in order to
change the type of the cursors (iterators) from pointer (not supported in SPARK)
to index into the array storing the container.
For example, the API of 'Element function is 
: cursor -> data for Ada 2012 Vectors
: Vector x Index -> data for SPARK.
Notice that SPARK specifications shall be executable.
To be more precise, the formal containers are implemented as follows:
- Vectors = continuous arrays 
- Dll = array with links denoted by indices
- Map, Sets = linear data structures for storing but 
              RBTrees for organization of the array

The formal proof of the implementation of formal containers is
a challenge to be considered by this project. The implementation
of each container is ~ 2KLOC.

For the moment, these containers are specified using a Why3
axiomatization and implemented in Why3 code. This generic code 
is called in proofs, the implementation code is called
in executable proofs.
In 2010, Claire Dross proved using Coq, for the version 2010 of this code
that the axiomatization is consistent. This proof of consistency is obsolete
for the new version of containers.

The applications using SPARK containers are verified by translation to
Why3 (made in the Hi-lite project) and then use of Alt-Ergo and CVC4 solvers.
Interface with Coq and Isabelle is also provided and used for proofs.
Claire Dross has proposed a way of translating the SPARK axioms such
that universal quantification is dealt using triggers by the SMT solvers.


'''''''''''''''''''''''''''''
Discussion on other case studies
'''''''''''''''''''''''''''''

Suggestions:
* C library glib, see also [Tafat 2013 PhD]
* C++ library STL (rewritten)
* Java library Containers (rewritten)
* Data structures used in the Bind (open source) 
  has been considered in the CEA-LIST team


'''''''''''''''''''''''''''''
M. Lemerre: Abstract Interpretation tools in Frama-C
'''''''''''''''''''''''''''''
The last version of Frama-C includes:
- an API for the interface with abstract domains
- a fixpoint module over the AST of CIL
For the moment, the fixpoint engine is not working on recursive programs
because function calls are dealt by inlining.


-------------------------------------------------------------------
Task 1: Logical Tools
-------------------------------------------------------------------

Technical discussion on:
- Details of the SLIDE decision procedure (by A. Rogalewicz).
- Discussion on combining SLIDE and SPEN procedures.


-------------------------------------------------------------------
Project management
-------------------------------------------------------------------

(Discussed during the meeting)

'''''''''''''''''''''''''''''
Actions
'''''''''''''''''''''''''''''

***First deliverable***
- To be published at T0+3 (February 2015) on 
    * the collected case studies and
    * the benchmarks of low level implementations for collections.

Yannick will send a reference to the code of the container libraries presented.


***Next meeting***

In february, in order to finalize the first deliverable.
Suggested to be organized as follows:
- morning: around a scientific presentation by an invited person
- afternoon: working session on finalizing the deliverable.


***Web page and common repository***
Need for a non commercial site for the project allowing to define
- (public and private) web pages
- wiki
- git repository
- mailing list
- news

Yannick will sent a reference for the forge (GNATTracker ?) used by AdaCore.

All: propose other solutions.


***Communication***

All: please communicate to Radu any event concerning
- accepted papers
- new versions of tools
- case studies
- seminars organized by the partners and related to the project
  (will be sent on the mailing list of the project)

Example:
o 2nd february special seminar (1 day) on SMT solvers 
  for kickoff of the project ProofInUse [http://www.spark-2014.org/proofinuse]
  Speakers: C. Marché, Y. Moy, F. Bobot, S. Conchon, M. Deters, M. Brain