Vous pouvez vous abonner à nos annonces de séminaires: http://cambium.inria.fr/seminar.html Nos séminaires sont accessibles en ligne en direct: https://webconf.math.cnrs.fr/b/fra-ryy-fjn S É M I N A I R E ______ __ _ / ____/___ _____ ___ / /_ (_)_ ______ ___ / / / __ `/ __ `__ \/ __ \/ / / / / __ `__ \ / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / / \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C Lundi 30 août, 10h30 --------------- Alexandre Moine --------------- Inria Paris ================================================== Formalisation d’une structure de donnée transiente et de ses itérateurs en logique de séparation ================================================== Une structure de données transiente propose à la fois une interface éphémère et une interface persistante, tout en offrant des conversions efficaces entre les deux. Sek est une bibliothèque OCaml (disponible sur opam) qui propose des séquences transientes. L’implémentation de ces dernières repose sur des tableaux de capacité fixe, appelés chunks. Le partage de segments de chunks entre les différentes instances d’une structure est l’ingrédient clé pour des opérations efficaces. Cependant, un tel partage est un défi pour la formalisation. Dans cet exposé, je présenterai une preuve en logique de séparation avec crédits-temps de la correction fonctionnelle ainsi que de la complexité amortie d’une pile transiente et de ses itérateurs, reprenant les mécanismes utilisés par la bibliothèque Sek. Cette formalisation relève le défi du partage grâce à des arguments de monotonie et propose des spécifications permettant une invalidation sélective des itérateurs concurrents.