Skip to Main content Skip to Navigation
New interface
Conference papers

Abstraction and Genericity in Why3

Jean-Christophe Filliâtre 1 Andrei Paskevich 1 
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LRI - Laboratoire de Recherche en Informatique
Abstract : The benefits of modularity in programming-abstraction barriers, which allows hiding implementation details behind an opaque interface, and genericity, which allows specializing a single implementation to a variety of underlying data types-apply just as well to deduc-tive program verification, with the additional advantage of helping the automated proof search procedures by reducing the size and complexity of the premises and by instantiating and reusing once-proved properties in a variety of contexts. In this paper, we demonstrate the modularity features of WhyML, the language of the program verification tool Why3. Instead of separating abstract interfaces and fully elaborated implementations, WhyML uses a single concept of module, a collection of abstract and concrete declarations , and a basic operation of cloning which instantiates a module with respect to a given partial substitution, while verifying its soundness. This mechanism brings into WhyML both abstraction and genericity, which we illustrate on a small verified Bloom filter implementation, translated into executable idiomatic C code.
Complete list of metadata
Contributor : Jean-Christophe Filliâtre Connect in order to contact the contributor
Submitted on : Monday, July 5, 2021 - 3:10:53 PM
Last modification on : Sunday, June 26, 2022 - 3:10:41 AM


Files produced by the author(s)



Jean-Christophe Filliâtre, Andrei Paskevich. Abstraction and Genericity in Why3. ISoLA 2021 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2021, Rhodes, Greece. ⟨10.1007/978-3-030-61362-4_7⟩. ⟨hal-02696246v2⟩



Record views


Files downloads