Properties¶

Each disco definition may have any number of associated properties, mathematical claims about the behavior of the definition which can be automatically verified by disco. Properties begin with !!!, must occur just before their associated definition, and may be arbitrarily interleaved with documentation lines beginning with |||.

Unit tests¶

The simplest kind of property is just an expression of type Bool, which essentially functions as a unit test. When loading a file, disco will check that all such properties evaluate to true, and present an error message if any do not.

example/unit-test.disco¶

!!! gcd(7,6)   == 1
!!! gcd(12,18) == 6
!!! gcd(0,0)   == 0

gcd : N * N -> N
gcd(a,0) = a
gcd(a,b) = gcd(b, a mod b)

When we load this file, disco reports that it successfully ran the tests associated with gcd:

Disco> :load example/unit-test.disco
Loading example/unit-test.disco...
Running tests...
  gcd: OK
Loaded.

On the other hand, if we change the first property to !!! gcd(7,6) = 2 and load the file again, we get an error:

Disco> :load example/unit-test.disco
Loading example/unit-test.disco...
Running tests...
  gcd:
  - Test result mismatch for: gcd (7, 6) = 2
    - Expected: 2
    - But got:  1
Loaded.

Quantified properties¶

More generally, properties can contain universally quantified variables. The syntax for a universally quantified property is as follows:

the word forall (or the Unicode symbol ∀);
one or more comma-separated bindings, each consisting of a variable name, a colon, and a type;
a period;
and an arbitrary expression, which should have type Bool and which may refer to the variables bound by the forall.

Such quantified properties have the obvious logical interpretation: they hold only if the given expression evaluates to true for all possible values of the quantified variables.

example/property.disco¶

!!! ∀ x:Bool. neg (neg x) == x
neg : Bool -> Bool
neg x = not x

!!! ∀p: N + N. plusIsoR (plusIso p) == p
plusIso : N + N -> N
plusIso (left n) = 2n
plusIso (right n) = 2n + 1

!!! ∀n:N. plusIso (plusIsoR n) == n
plusIsoR : N -> N + N
plusIsoR n =
  {? left  (n // 2)   if 2 divides n
   , right (n // 2)   otherwise
  ?}

!!! forall x:N, y:N, z:N.
      f(f(x,y), z) == f(x, f(y,z))

f : N*N -> N
f (x,y) = x + x*y + y

In the example above, the first three properties have a single quantified variable, and specify respectively that neg is self-inverse, and plusIso and plusIsoR are inverse. The last function has a property with multiple quantified variables, and specifies that f is associative. Notice that as in this last example, properties may extend onto multiple lines, as long as subsequent lines are indented. Only a single !!! should be used at the start of each property.

Such properties may be undecidable in general, so disco cannot automatically prove them. Instead, it searches for counterexamples. If the input space is finite and sufficiently small (as in the first example above, which quantifies over a single boolean), disco will enumerate all possible inputs and check each one; so in this special case, disco can actually prove the property by exhaustively checking all cases. Otherwise, disco randomly generates a certain number of inputs (a la QuickCheck) and checks that the property is satisfied for each. If a counterexample is found, the property certainly does not hold, and the counterexample can be printed. If no counterexample is found, the property “probably” holds.

For example, consider this function with a property claiming it is associative:

example/failing/property.disco¶

!!! forall x:N, y:N, z:N.
      f(f(x,y), z) = f(x, f(y,z))

f : N*N -> N
f (x,y) = x + 2*y

The function is not associative, however, and if we try to load this file disco quickly finds a counterexample:

Disco> :load example/failing/property.disco
Loading example/failing/property.disco...
Running tests...
  f:
  - Test result mismatch for: ∀ x : ℕ, y : ℕ, z : ℕ. f (f (x, y), z) = f (x, f (y, z))
    - Expected: 5
    - But got:  3
    Counterexample:
      x = 1
      y = 0
      z = 1
Loaded.