property.bend relies on unsafe/foreign

raw source on the hub · import bend-kit-property@0.2.0.0/property.bend as Property

Reproducible property checks with generated inputs and greedy shrinking.

4 imports

import Base
import bend-kit-random@0.1.0.1/random.bend as Rand
import ./generate.bend as Gen
import ./shrink.bend as Shrink

Types

type Failure source · line 7 · raw

@-T:Type -> Type

Failure

@-T:Type -> @seed:U32 -> @trial:Nat -> @value:T -> Failure<T>

Templates

template smaller source · line 11 · raw

@-T:Type -> @-test:(@_:T -> Pair(T, Bool)) -> @xs:List<&1, T> -> @tested:Pair(T, Bool) -> Maybe<&1, T>

Scan candidates in order; a predicate returns its input so affine values work.

template smaller.start source · line 28 · raw

@-T:Type -> @-test:(@_:T -> Pair(T, Bool)) -> @xs:List<&1, T> -> Maybe<&1, T>

template attempt.pair source · line 35 · raw

@-T:Type -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @pair:Pair(T, T) -> Pair(T, Maybe<&1, T>)

template attempt source · line 39 · raw

@-T:Type -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @value:T -> Pair(T, Maybe<&1, T>)

template minimize source · line 43 · raw

@-T:Type -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @fuel:Nat -> @state:Pair(T, Maybe<&1, T>) -> T

Each accepted failure restarts shrinking; fuel bounds user-supplied shrinkers.

template minimize.start source · line 57 · raw

@-T:Type -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @value:T -> T

template draw.pair source · line 61 · raw

@-T:Type -> @-test:(@_:T -> Pair(T, Bool)) -> @pair:Pair(T, 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng) -> Pair(Pair(T, Bool), 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)

template draw source · line 65 · raw

@-T:Type -> @-gen:(@_:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Pair(T, 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)) -> @-test:(@_:T -> Pair(T, Bool)) -> @rng:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Pair(Pair(T, Bool), 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)

template check.go source · line 68 · raw

@-T:Type -> @-gen:(@_:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Pair(T, 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)) -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @remaining:Nat -> @+seed:U32 -> @+trial:Nat -> @state:Pair(Pair(T, Bool), 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng) -> Maybe<&1, Failure<T>>

template check.start source · line 93 · raw

@-T:Type -> @-gen:(@_:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Pair(T, 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)) -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @remaining:Nat -> @seed:U32 -> @rng:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Maybe<&1, Failure<T>>

template check source · line 103 · raw

@-T:Type -> @-gen:(@_:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Pair(T, 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)) -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @+seed:U32 -> @trials:Nat -> Maybe<&1, Failure<T>>

Return the first failure and its smallest reachable counterexample.

template report source · line 109 · raw

@-T:Type -> @-show:(@_:T -> String) -> @result:Maybe<&1, Failure<T>> -> IO(Bool)

Print the seed and draw index so a failing check can be replayed.

template run source · line 118 · raw

@-T:Type -> @-gen:(@_:0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng -> Pair(T, 0x46b9429cbffa7a8c1111ce19c60a3d6a/random.Rng)) -> @-copy:(@_:T -> Pair(T, T)) -> @-shrink:(@_:T -> List<&1, T>) -> @-test:(@_:T -> Pair(T, Bool)) -> @-show:(@_:T -> String) -> @seed:U32 -> @trials:Nat -> IO(Bool)