2026-07-20T05:27:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3170 2024-03-06T10:33:54Z ddc:004 open_access

Smart test data generators via logic programming Bulwahn, Lukas specification-based testing functional programming We present a novel counterexample generator for the interactive theorem prover Isabelle based on a compiler that synthesizes test data generators for functional programming languages (e.g. Standard ML, OCaml) from specifications in Isabelle. In contrast to naive type-based test data generators, the smart generators take the preconditions into account and only generate tests that fulfill the preconditions. The smart generators are constructed by a compiler that reformulates the preconditions as logic programs and analyzes them by an enriched mode inference. From this inference, the compiler can construct the desired generators in the functional programming language. These test data generators are applied to find errors in specifications, as we show in a case study of a hotel key card system. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lukas Bulwahn 2011 Is Part Of LIPIcs, Volume 11, Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICLP.2011.139 urn:nbn:de:0030-drops-31703 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2011.139 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode