Abstract
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.
A. Paskevich—This research was partly supported by the French National Research Organization (project VOCAL ANR-15-CE25-008) and by the Inria-Mitsubishi Electric bilateral contract “ProofInUse-MERCE”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
“Cabbage hash can be delicious,” said Alice, “but I would never dare to hash a king.”.
- 2.
In this case, due to the specifics of state handling in WhyML, not even abstract functions are allowed to announce a potential write in the
field, which limits the usefulness of this kind of construction. This may be relaxed in the future.
References
Abrial, J.-R.: The B-Book, Assigning Programs to Meaning. Cambridge University Press, Cambridge (1996)
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6
Ancona, D., Zucca, E.: An algebraic approach to mixins and modularity. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 179–193. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61735-3_12
Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422–426 (1970)
Chrzaszcz, J.: Modules in Type Theoryx with Generative Definitions. Ph.D. thesis, Warsaw University, Poland and Université de Paris-Sud (January 2004)
Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4
Koenig, J., Rustan, K., Leino, M.: Programming language features for refinement. In: Derrick, J., Boiten, E.A., Reeves, S. (eds.) Proceedings of 17th International Workshop on Refinement, Refine@FM 2015. EPTCS, Oslo, Norway, 22 June 2015, vol. 209, pp. 87–106 (2015)
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20
Leino, K.R.M., Matichuk, D.: Modular verification scopes via export sets and translucent exports. In: Müller, P., Schaefer, I. (eds.) Principled Software Development, pp. 185–202. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98047-8_12
Leroy, X.: A modular module system. J. Funct. Program. 10(3), 269–303 (2000)
Louridas, P.: Real-World Algorithms: A Beginner’s Guide. The MIT Press, Cambridge (2017)
Mitzenmacher, M., Upfal, E.: Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, New York (2005)
Rieu-Helft, R., Marché, C., Melquiond, G.: How to get an efficient yet verified arbitrary-precision integer library. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 84–101. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_6
Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.P.: Traits: composable units of behaviour. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 248–274. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45070-2_12
Mohamed, O.A., Muñoz, C., Tahar, S. (eds.): TPHOLs 2008. LNCS, vol. 5170. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7
Wadler, P., Blott. S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1889, pp. 60–76. ACM, New York (1989)
Acknowledgments
We are grateful to Claude Marché, Jacques-Henri Jourdan, and Rustan Leino for their insightful remarks and suggestions.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Filliâtre, JC., Paskevich, A. (2020). Abstraction and Genericity in Why3. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. ISoLA 2020. Lecture Notes in Computer Science(), vol 12476. Springer, Cham. https://doi.org/10.1007/978-3-030-61362-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-61362-4_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-61361-7
Online ISBN: 978-3-030-61362-4
eBook Packages: Computer ScienceComputer Science (R0)