Résumé
Une structure de données persistante permet de faire coexister plusieurs versions qui partagent une histoire, c'est-à-dire des ancêtres communs, là où une structure éphémère ne donne accès qu'à la version la plus récente.
Cet exposé présente la notion de structure semi-persistante, où on limite l'accès aux ancêtres de la version la plus récente. Une structure semi-persistante reste en particulier adaptée à un algorithme de retour sur trace. Plusieurs exemples de structures semi-persistantes sont présentés, et le gain en temps et en espace est illustré.
Pour garantir le bon usage d'une structure semi-persistante, on adopte une approche déductive où des annotations logiques dans le programme expriment les relations de parenté entre les versions de la structure. On donne une procédure de décision pour les obligations de preuve qui en résultent.
