Foundational Property-Based Testing
| Autor: | Cătălin Hriţcu, Maxime Dénès, Zoe Paraskevopoulou, Leonidas Lampropoulos, Benjamin C. Pierce |
|---|---|
| Přispěvatelé: | École normale supérieure - Cachan (ENS Cachan), Programming securely with cryptography (PROSECCO), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Programming languages, types, compilation and proofs (GALLIUM), University of Pennsylvania [Philadelphia], University of Pennsylvania |
| Rok vydání: | 2015 |
| Předmět: | |
| Zdroj: | Interactive Theorem Proving ISBN: 9783319221014 ITP ITP 2015-6th conference on Interactive Theorem Proving ITP 2015-6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_22⟩ |
| Popis: | International audience; Integrating property-based testing with a proof assistant creates an interesting opportunity: reusable or tricky testing code can be formally verified using the proof assistant itself. In this work we introduce a novel methodology for formally verified property-based testing and implement it as a foundational verification framework for QuickChick, a port of QuickCheck to Coq. Our framework enables one to verify that the executable testing code is testing the right Coq property. To make verification tractable, we provide a systematic way for reasoning about the set of outcomes a random data generator can produce with non-zero probability, while abstracting away from the actual probabilities. Our framework is firmly grounded in a fully verified implementation of QuickChick itself, using the same underlying verification methodology. We also apply this methodology to a complex case study on testing an information-flow control abstract machine, demonstrating that our verification methodology is modular and scalable and that it requires minimal changes to existing code. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|