| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The use of several libraries at the same time via the common interface and the managers associated to each library raises the problem of typing. Look at the following code:
ap_manager_t* manpk = pk_manager_alloc(true); /* manager for Polka */
ap_manager_t* manoct = oct_manager_alloc(); /* manager for octagon */
ap_abstract0_t* abs1 = ap_abstract_top(manpk,3,3);
ap_abstract0_t* abs2 = ap_abstract_top(manoct,3,3);
bool b = ap_abstract0_is_eq(manoct,abs1,abs2);
/* Problem: the effective function called (octagon_is_eq) expects
abs1 to be an octagon, and not a polyhedron ! */
ap_abstract0_t* abs3 = ap_abstract_top(manoct,3,3);
abstract0_meet_with(manpk,abs2,abs3);
/* Problem: the effective function called (pk_meet_with) expects
abs2 and abs3 to be polyhedra, but they are octagons */
|
There is actually no static typing, as abstract0_t*
and manager_t are abstract types shared by the different
libraries. Types are thus dynamically checked by the interface.
Notice that the use of C++ and inheritance would not solve
directly the problem, if functions of the interface are methods of
the manager; one would have:
ap_manager_t* manpk = pk_manager_alloc(true);
/* manager for Polka, effective type pk_manager_t* */
ap_manager_t* manoct = oct_manager_alloc();
/* manager for octagon, effective type oct_manager_t* */
ap_abstract0_t* abs1 = manpk->abstract_top(3,3);
/* effective type: poly_t */
ap_abstract0_t* abs2 = manoct->abstract_top(3,3);
/* effective type: oct_t */
bool b = manoct->abstract0_is_eq(abs1,abs2);
/* No static typing possible:
manpk->abstract0_is_eq and manoct->abstract0_is_eq should have the same
signature (otherwise one cannot interchange manpk and manoct in the code),
which means that abs1 and abs2 are supposed to be of type abstract0_t* */
*/
|
Currently, only the OCaml polymorphic type system allows to solve elegantly this problem.