API Reference
Quantifier module
exists(**binds)
Decorates a predicate funcion or another decorator with an existencial quantifier.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
**binds |
The quantified variables. The number of quantified
variables must be 1. In order to quantify more than
one variable, you should write each variable in its own
|
{}
|
Returns:
| Type | Description |
|---|---|
Exists
|
An object implementing the property as a callable. |
Warning
Every variable must be quantified over an exhaustible domain.
forall(n_samples: int = DEFAULT_N_SAMPLES, **binds)
Decorates a predicate funcion or another decorator with a forall quantifier.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n_samples |
int
|
The number of samples to check. |
DEFAULT_N_SAMPLES
|
**binds |
The quantified variables. The number of quantified
variables must be 1. In order to quantify more than
one variable, you should write each variable in its own
|
{}
|
Returns:
| Type | Description |
|---|---|
ForAll
|
An object implementing the property as a callable. |
Domain module
Domain
Bases: Generic[T]
Domain abstract class
This is the base class for every Domain. It includes some
operations like union.
It also includes the method that to decorate a domain with extra
funcionality. For example: limiting the number of samples that it
will generate.
Exhaustible vs non-exhaustible
By default, domains are non exhaustibles. Thus, their attribute
is_exhaustible = False and they do not implement any exhaustible
iterator. Exhaustible Domains set that attribute to True
themselves. When a domain may be exhaustible, includes a parameter
in the __init__ function. And, of course, implements the
exhaustible iterator.
__iter__() -> Iterator[T]
Returns the cannonical iterator for a domain.
This is the magic method of any python iterable. The returned iterator is the pbt cannonical one. This iterator will pick and yield random samples from the domain.
exhaustible() -> Iterator[T]
property
Returns an iterator that can be exhausted.
The Domain must be marked as exhaustible. The library cannot infer whether a Domain is exhaustible.
Warning
Forcing the exhaustible attribute on a Domain that does not implement the exhaustible iterator will result in an exception when trying to use this property.
exhaustible_iter() -> Iterator[T]
Returns the non-cannonical, exhaustible iterator for a domain.
The returned iterator is not the pbt cannonical one. Instead of picking random samples, this iterator will pick and yield all the elements of the domain.
NOTE that most domains can not be exhausted because the number of elements is too big, generating them is too costly, or, most of the cases, the number of elements is infinite.
WARNING do not use this method directly, instead use the
property exhaustible.
that(samples_limit: int) -> Domain
Decorate this domain
Returns a decorator of this domain. The decorator will change the behaviour of the domain based on the given parameters.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
samples_limit |
int
|
max number of samples the domain generates. See [DomainLimit] |
required |
Returns:
| Type | Description |
|---|---|
Domain
|
the decorated domain |
DomainLimit
Bases: Domain
Modify a Domain in order to limit the number of generated samples.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
samples_limit |
int
|
max number of samples each iterator will yield |
required |
Tuple
Bases: Domain
Domain of n-tuples.
Implements the sum, not the product.
I.e. tuple(Dom([1,2,...]),Dom(['a','b',...]))
may yield: (1,'b'), (2,'a'), but not: (1,'a'),(1,'b'),(2,'a'),(2,'b').
Note that it is not possible to implement the product of non-exhaustible domains.
domain_expr(arg: DomainCoercible, is_exhaustible: Optional[bool] = None) -> Domain
Desugar domain expressions
Converts any expression declaring a domain into a Domain object. The options are:
-
If arg is already a Domain object, returns it. Parameters are not allowed.
-
If arg is any python iterable, returns a Domain object whose elements are the items in the iterable. The programmer may mark the domain as exhaustible when neccessary.
-
If arg is a generator function, equivalent to iterable, taking the elements from the generator returned by the function.
-
If arg is any other python object, returns a Domain containing only one element: arg.