SciFe

SciFe is capable of exhaustive, memoized enumeration of values from finite or infinite domains. SciFe introduces concepts of enumerators and enumerator combinators. SciFe is a Scala library that implements a domain-specific language. SciFe can generate complex structures such as search trees and models of class hierarchies. Specifications in SciFe are short and lead to very efficient enumeration, even in case of complex data structures with invariants.

SciFe logo

Overview

SciFe is a Scala library that implements a domain specific language for automated generation of complex structures, suitable for tasks such as automated testing and synthesis.

Example usage

SciFe uses enumerators and combinators to define data generation. The following example of enumerating all valid date objects starting from the first day of 2014.:

val dates = (1 to 31) ⊗ (1 to 12) ⊗ Stream.from(2014) ≻
  { isValid(_) } ↑ { case ((d, m), y) ⇒ new Date(y, m, d) }

Encoded dates can easily be enumerated with:

for (i ← 0 until 5) yield dates(i) // get first 5 days
dates(208) // get 208th date

dates.hasDefiniteSize // returns false
for (d ← dates) yield print(d) // prints all dates (does not stop)

SciFe can also enumerate complex structures such as binary search trees:

rec[(Int, Range), Tree]({ case ((size, range), self) ⇒ {
  if (size == 0) Leaf
  else {
    val left: Depend[(Int, Int), Tree] = self ↓
      { case (ls, m) ⇒ (ls, range.start to (m−1)) }
    val right: Depend[(Int, Int), Tree] = self ↓
      { case (ls, m) ⇒ (size − ls − 1, (m+1) to range.end) }

    left ⊗ right ⊘ ((0 until size) ⊗ range) ↑ {
      case (( , root), (lt, rt)) ⇒ Node(lt, root, rt) }
}}})

This code enumerates all valid trees of size 15, more than 9.6·106 of those, in just a few seconds.
 

SciFe in more details

SciFe is capable of exhaustive, memoized enumeration of values from finite or infinite domains. SciFe introduces concepts of enumerators and enumerator combinators. SciFe is a Scala library that implements a domain-specific language. SciFe can generate complex structures such as search trees and models of class hierarchies. Specifications in SciFe are short and lead to very efficient enumeration, even in case of complex data structures with invariants.

Features

  • SciFe can outperform test generation tools in terms of lenth of specification and performance; up to 10x shorter specification and 3 orders of magnitude speedup in case of Korat and 3x and 2 orders of magnitude in case of constraint-logic programming approach.
  • Modularity allows treating enumerators as self-contained building blocks.
  • Memoization allows storing and sharing computed intermediate results.
  • Random access allows random testing, in addition to exhaustive enumeration.
  • Fine-grain enumeration offers precise choice of which instances to enumerate.

Benchmarks

Benchmarks results (accumulated over multiple runs) can be viewed at. Tables summarize the comparison of measured performance. Data structures were generated with SciFe (with memoization enabled), the constraint logic programming approach (CLP), and Korat (see publication for more details). Benchmark data are available at. Benchmarks can be run at any time by running

sbt bench:test