QuickSpec: guessing formal specifications using testing. We present QuickSpec, a tool that automatically generates algebraic specifications for sets of pure functions. The tool is based on testing, rather than static analysis or theorem proving. The main challenge QuickSpec faces is to keep the number of generated equations to a minimum while maintaining completeness. We demonstrate how QuickSpec can improve one’s understanding of a program module by exploring the laws that are generated using two case studies: a heap library for Haskell and a fixed-point arithmetic library for Erlang.

References in zbMATH (referenced in 7 articles )

Showing results 1 to 7 of 7.
Sorted by year (citations)

  1. Johansson, Moa: Lemma discovery for induction. A survey (2019)
  2. Smallbone, Nicholas; Johansson, Moa; Claessen, Koen; Algehed, Maximilian: Quick specifications for the busy programmer (2017)
  3. Grechanik, S. A.: Proving properties of functional programs by equality saturation (2015)
  4. Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
  5. Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
  6. Page, Rex: Property-based testing and verification: a catalog of classroom examples (2012) ioport
  7. Claessen, Koen; Smallbone, Nicholas; Hughes, John: QuickSpec: guessing formal specifications using testing (2010) ioport