License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICLP.2011.139
URN: urn:nbn:de:0030-drops-31703
Go to the corresponding LIPIcs Volume Portal

Bulwahn, Lukas

Smart test data generators via logic programming

13.pdf (0.5 MB)


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.

BibTeX - Entry

  author =	{Lukas Bulwahn},
  title =	{{Smart test data generators via logic programming}},
  booktitle =	{Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) },
  pages =	{139--150},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-31-6},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{11},
  editor =	{John P. Gallagher and Michael Gelfond},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-31703},
  doi =		{10.4230/LIPIcs.ICLP.2011.139},
  annote =	{Keywords: specification-based testing, functional programming}

Keywords: specification-based testing, functional programming
Collection: Technical Communications of the 27th International Conference on Logic Programming (ICLP'11)
Issue Date: 2011
Date of publication: 27.06.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI