Data Abstraction: A General Framework to Handle Program Verification of Data Structures

Proving properties on programs accessing data structures such as arrays often requires universally quantified invariants, e.g., "all elements below index $i$ are nonzero''. In this research report, we propose a general data abstraction scheme operating on Horn formulas, into which we recast previously published abstractions. We show our instantiation scheme is relatively complete: the generated purely scalar Horn clauses have a solution (inductive invariants) if and only if the original problem has one expressible by the abstraction.Pour prouver des propriétés de programmes qui manipulent des structures de données comme des tableaux , nous avons besoin de savoir résoudre des formules comportant des quantificateurs universels: par exemple, “tous les éléments d’index inférieur à $i$ sont différents de 0”. Dans ce rapport de recherche, nous proposons une technique générale d’abstraction opérant sur des Clauses de Horn, qui permet de reformuler un certain nombre d’abstractions déjà publiées. Nous montrons que notre schéma d’abstraction est relativement complet: le système de clauses purement scalaires a une solution (sous forme d’invariants inductifs) si et seulement si le problème initial a une solution exprimable dans la logique de l’abstraction