nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Abstraction and Genericity in Why3

verfasst von : Jean-Christophe Filliâtre, Andrei Paskevich

Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Assumption-Commitment Types for Resource Management in Virtually Timed Ambients

Nächstes Kapitel Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework

“Cabbage hash can be delicious,” said Alice, “but I would never dare to hash a king.”.

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

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-61362-4_7/MediaObjects/505126_1_En_7_Figdj_HTML.gif

field, which limits the usefulness of this kind of construction. This may be relaxed in the future.

Abrial, J.-R.: The B-Book, Assigning Programs to Meaning. Cambridge University Press, Cambridge (1996)CrossRef

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-6CrossRef

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_12CrossRefMATH

Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422–426 (1970)CrossRef

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_8CrossRef

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_4CrossRef

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_20CrossRefMATH

10.

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_12CrossRef

11.

Leroy, X.: A modular module system. J. Funct. Program. 10(3), 269–303 (2000)CrossRef

12.

Louridas, P.: Real-World Algorithms: A Beginner’s Guide. The MIT Press, Cambridge (2017)MATH

13.

Mitzenmacher, M., Upfal, E.: Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, New York (2005)CrossRef

14.

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_6CrossRefMATH

15.

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_12CrossRef

16.

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-7CrossRef

17.

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)

Titel: Abstraction and Genericity in Why3
verfasst von: Jean-Christophe Filliâtre
Andrei Paskevich
Verlag: Springer International Publishing
Buch: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles
Print ISBN: 978-3-030-61361-7

Electronic ISBN: 978-3-030-61362-4

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-61362-4_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner