The New Quickcheck for Isabelle

Autor:	Lukas Bulwahn
Rok vydání:	2012
Předmět:	Test strategy Class (computer programming) Theoretical computer science Computer science Test data generation Random testing HOL Executable computer.file_format Data structure computer Counterexample
Zdroj:	Certified Programs and Proofs ISBN: 9783642353079 CPP
DOI:	10.1007/978-3-642-35308-6_10
Popis:	The new Quickcheck is a counterexample generator for Isabelle/HOL that uncovers faulty specifications and invalid conjectures using various testing strategies. The previous Quickcheck only tested conjectures by random testing. The new Quickcheck extends the previous one and integrates two novel testing strategies: exhaustive testing with concrete values; and symbolic testing, evaluating conjectures with a narrowing strategy. Orthogonally to the strategies, we address two general issues: First, we extend the class of executable conjectures and specifications, and second, we present techniques to deal with conditional conjectures, i.e., conjectures with premises. We evaluate the testing strategies and techniques on a number of specifications, functional data structures and a hotel key card system.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::79fd91409ce423c4c3dfacc1fe4a6686 https://doi.org/10.1007/978-3-642-35308-6_10 Zobrazit plný text záznamu