TY - GEN
T1 - Abstraction and Genericity in Why3
AU - Filliâtre, Jean Christophe
AU - Paskevich, Andrei
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - The benefits of modularity in programming—abstraction barriers, which allow 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 deductive 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.
AB - The benefits of modularity in programming—abstraction barriers, which allow 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 deductive 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.
U2 - 10.1007/978-3-030-61362-4_7
DO - 10.1007/978-3-030-61362-4_7
M3 - Conference contribution
AN - SCOPUS:85097367207
SN - 9783030613617
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 122
EP - 142
BT - Leveraging Applications of Formal Methods, Verification and Validation
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Science and Business Media Deutschland GmbH
T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
Y2 - 20 October 2020 through 30 October 2020
ER -