Typer la désérialisation sans sérialiser les types
Nous proposons dans cet article une façon d'attribuer un type statique à des fonctions de désérialisation, et développons une technique de vérification des données désérialisées qui préserve la sûreté d'exécution garantie par le typage statique. Cette technique repose sur un type singleton dont la valeur est transmise à l'exécution aux fonctions de désérialisation, ainsi que sur un algorithme de vérification dynamique efficace capable de traiter le partage et les cycles, dont nous prouvons la correction.
In this paper, we propose a way of assigning static type information to unmarshalling functions and we describe a verification technique for unmarshalled data that preserves the execution safety provided by static type checking. This technique, whose correctness is proven, relies on singleton types whose values are transmitted to unmarshalling routines at runtime, and on an efficient checking algorithm able to deal with sharing and cycles.
G.HENRY, M.MAUNY, E.CHAILLOUX
Reçu le 19 avril 2006.
Accepté le 15 février 2007.
sérialisation, désérialisation, typage statique, anti-unification, ML, OCaml, récursion polymorphe.
marshalling, unmarshalling, static typing, antiunification, ML, OCaml, polymorphic recursion.
Français
|
