Top

Software Quality Journal

Published in:

22-02-2022

Towards random and enumerative testing for OCaml and WhyML properties

Authors: Clotilde Erard, Alain Giorgetti, Jérome Ricciardi

Published in: Software Quality Journal | Issue 1/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Deductive program verification greatly improves software quality, but proving formal specifications is difficult, and this activity can only be partially automated. It is therefore relevant to supplement deductive verification tools, such as Why3, with the ability to test the properties to be verified. We present a methodological study and a prototype for the random and enumerative testing of properties written either in the Why3 input language WhyML or in the OCaml programming language used by Why3 to run programs written in WhyML. An originality is that we propose enumerative testing based on data generators themselves written in WhyML and formally verified with Why3. Another specificity is that the development effort is reduced by exploiting Why3’s extraction mechanism to OCaml and an existing random testing tool for OCaml. These design choices are applied in a prototypal implementation of a tool, called AutoCheck. The prototype and the paper are designed with simplicity and usability in mind, in order to make them accessible to the widest audience. Starting from the most elementary cases, a tutorial illustrates the implemented features with many examples presented in increasing complexity order.

previous article Ontology-based metamorphic testing for chatbots

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

http://why3.lri.fr/stdlib/bool.html.

http://toccata.lri.fr/gallery/inverse_in_place.en.html, April 30, 2021

In the folder https://gitlab.inria.fr/why3/why3/-/blob/1.4.0/examples.

Arndt, J. (2010). Matters Computational - Ideas, Algorithms, Source Code [The Fxtbook]. https://www.jjj.de/fxt/fxtpage.html

Barnett, M., Leino, K., & Schulte, W. (2004). The spec# programming system: An overview. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS’04), Lecture Notes in Computer Science, vol. 3362, pp. 49–69. Springer-Verlag, Marseille, France

Beckert, B., Hähnle, R., & Schmitt, P. H. (eds.) (2007). Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science, vol. 4334. Springer, Heidelberg.

Blatter, L., Kosmatov, N., Le Gall, P., Prevosto, V., & Petiot, G. (2018). Static and dynamic verification of relational properties on self-composed C code. In: C. Dubois, B. Wolff (eds.) Tests and Proofs. TAP 2018, pp. 44–62. Springer International Publishing, Cham. https://doi.org/10.1007/978-3-319-21215-9_7

Bulwahn, L. (2012). The new Quickcheck for Isabelle - random, exhaustive and symbolic testing under one roof. In: C. Hawblitzel, D. Miller (eds.) CPP 2012, Lecture Notes in Computer Science, vol. 7679, pp. 92–108. Springer, Heidelberg, Kyoto, Japan. https://doi.org/10.1007/978-3-642-35308-6_10

Claessen, K., & Hughes, J. (2000). QuickCheck: A lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Not., vol. 35, pp. 268–279. ACM, New York. https://doi.org/10.1145/351240.351266

Clarke, E.M., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Lecture Notes in Computer Science, vol. 2988, pp. 168–176. Springer. https://doi.org/10.1007/978-3-540-24730-2_15

Correnson, L. (2014). Qed. Computing what remains to be proved. In: J.M. Badger, K.Y. Rozier (eds.) NFM 2014, Lecture Notes in Computer Science, vol. 8430, pp. 215–229. Springer, Heidelberg. http://dx.doi.org/10.1007/978-3-319-06200-6_17

Dijkstra, E. W. (1976). A Discipline of Programming. In: Series in Automatic Computation. Prentice Hall.

Dubois, C., & Giorgetti, A. (2018). Tests and proofs for custom data generators. Formal Aspects of Computing 30(6), 659–684. https://doi.org/10.1007/s00165-018-0459-1

Dubois, C., Giorgetti, A., & Genestier, R. (2016). Tests and proofs for enumerative combinatorics. In: K.B. Aichernig, A.C. Furia (eds.) Tests and Proofs. TAP 2016, Lecture Notes in Computer Science, vol. 6792, pp. 57–75. Springer, Cham. https://doi.org/10.1007/978-3-319-41135-4_4

Duregård, J., Jansson, P., & Wang, M. (2012). Feat: functional enumeration of algebraic types. In: Proceedings of the 2012 Haskell Symposium, ACM SIGPLAN Notices, vol. 47, pp. 61–72. Association for Computing Machinery, New York, NY, USA. https://doi.org/10.1145/2364506.2364515

Erard, C., & Giorgetti, A. (2019). Bounded exhaustive testing with certified and optimized data enumeration programs. In: Testing Software and Systems. ICTSS 2019., Lecture Notes in Computer Science, vol. 11812, pp. 159–175. Springer, Cham. https://doi.org/10.1007/978-3-030-31280-0_10

Filliâtre, J. -C., & Pereira, M. (2016) Itérer avec confiance. In: Journées Francophones des Langages Applicatifs. JFLA. https://hal.inria.fr/hal-01240891

Filliâtre, J. -C., & Pereira, M. (2016). A modular way to reason about iteration. In: S. Rayadurgam, O. Tkachuk (eds.) NFM 2016, Lecture Notes in Computer Science, vol. 9690, pp. 322–336. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_24

Fitinghoff, N. (2019). Extraction of Rust code from the Why3 verification platform. Ph.D. thesis, Luleå University of Technology. http://www.diva-portal.org/smash/get/diva2:1303268/FULLTEXT02#page20

Genestier, R., Giorgetti, A., & Petiot, G. (2015). Sequential generation of structured arrays and its deductive verification. In: J.C. Blanchette, N. Kosmatov (eds.) Tests and Proofs. TAP 2015, Lecture Notes in Computer Science, vol. 9154, pp. 109–128. Springer, Cham. https://doi.org/10.1007/978-3-319-21215-9_7

Giorgetti, A., Dubois, C., & Lazarini, R. (2019). Combinatoire formelle avec Why3 et Coq. In: N. Magaud, Z. Dargaye (eds.) Journées Francophones des Langages Applicatifs. JFLA 2019., pp. 139–154. https://hal.inria.fr/hal-01985195

Giorgetti, A., & Lazarini, R. (2018). Preuve de programmes d’énumération avec Why3. In: AFADL 2018, pp. 14–19. http://afadl2018.ls2n.fr/wp-content/uploads/sites/38/2018/06/AFADL_Procs_2018.pdf

Hauzar, D., Marché, C., & Moy, Y. (2016). Counterexamples from proof failures in SPARK. In: R. De Nicola, E. Kühn (eds.) Software Engineering and Formal Methods. SEFM 2016, Lecture Notes in Computer Science, vol. 9763, pp. 215–233. Springer, Cham. https://hal.inria.fr/hal-01314885

Herdt, V., Große, D., Le, H. M., & Drechsler, R. (2019). Verifying instruction set simulators using coverage-guided fuzzing(^*). In: J. Teich, F. Fummi (eds.) Design, Automation & Test in Europe Conference & Exhibition, DATE 2019, Florence, Italy, March 25-29, 2019, pp. 360–365. IEEE. https://doi.org/10.23919/DATE.2019.8714912

Knuth, D. E. (1997). The Art of Computer Programming, Volume 1 (3rd Ed.): Fundamental Algorithms. Addison Wesley Longman Publishing Co., Inc., USA.

Kosmatov, N., Marché, C., Moy, Y., & Signoles, J. (2016). Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: T. Margaria, B. Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Lecture Notes in Computer Science, vol. 9952, pp. 461–478. Springer and Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_32

Leavens, G. T., Baker, A. L., & Ruby, C. (1999). JML: A notation for detailed design. In H. Kilov, B. Rumpe, & I. Simmonds (Eds.), Behavioral Specifications of Businesses and Systems (pp. 175–188). Boston: Kluwer Academic Publishers.CrossRef

Leino, K. R. M., & Moskal, M. (2010). Usable auto-active verification. In: Usable Verification Workshop. http://fm.csl.sri.com/UV10/

Midtgaard, J., & Møller, A. (2017). QuickChecking static analysis properties. Software Testing, Verification and Reliability 27(6), e1640. https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.1640

Nelson, J. (2017). The design and use of QuickCheck. Blog post https://begriffs.com/posts/2017-01-14-design-use-quickcheck.html

Padhye, R., Lemieux, C., & Sen, K. (2019). JQF: Coverage-guided property-based testing in Java. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, pp. 398–401. Association for Computing Machinery, New York, NY, USA. https://doi.org/10.1145/3293882.3339002

Pereira, M. J. P. (2018) Tools and techniques for the verification of modular stateful code. Ph.D. thesis, Université Paris-Sud. https://tel.archives-ouvertes.fr/tel-01980343/document

Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., & Julliand, J. (2018). How testing helps to diagnose proof failures. Formal Aspects of Computing 30(6), 629–657. https://doi.org/10.1007/s00165-018-0456-4

Rebours, N. (2019). An introduction to fuzzing OCaml with AFL, Crowbar and Bun. https://tarides.com/blog/2019-09-04-an-introduction-to-fuzzing-ocaml-with-afl-crowbar-and-bun

Reich, J. S., Naylor, M., & Runciman, C. (2013). Advances in Lazy SmallCheck. In: R. Hinze (ed.) Implementation and Application of Functional Languages. IFL 2012., Lecture Notes in Computer Science, vol. 8241, pp. 53–70. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41582-1_4

Rieu-Helft, R. (2018). Un mécanisme d’extraction vers C pour Why3. In: Journées Francophones des Langages Applicatifs. JFLA 2018., pp. 203–209. https://hal.inria.fr/hal-01707376v1

Runciman, C., Naylor, M., & Lindblad, F. (2008). SmallCheck and Lazy SmallCheck - automatic exhaustive testing for small values. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, pp. 37–48. ACM. https://doi.org/10.1145/1411286.1411292

Title: Towards random and enumerative testing for OCaml and WhyML properties
Authors: Clotilde Erard
Alain Giorgetti
Jérome Ricciardi
Publication date: 22-02-2022
Publisher: Springer US
Published in: Software Quality Journal / Issue 1/2022
Print ISSN: 0963-9314
Electronic ISSN: 1573-1367
DOI: https://doi.org/10.1007/s11219-021-09572-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Other articles of this Issue 1/2022

Using knowledge discovery to propose a two-phase model checking for safety analysis of graph transformations

Evaluating the complexity of deriving adaptive -homing and -synchronizing sequences for nondeterministic FSMs

An autonomous performance testing framework using self-adaptive fuzzy reinforcement learning

Evaluation of alternative design choices for evolutionary mutation testing by means of automated configuration

Machine learning techniques for software testing effort prediction

Ontology-based metamorphic testing for chatbots

Premium Partner