Limitations of Targeted Properties

Limitations of targeted properties

Targeted properties do not allow all the same facilities as we’d get with regular properties. They don’t work well with recursive generators, whether we use ?LAZY or not. Using that combination may yield infinite loops. In those cases, it is best to stick to rather straightforward combinations of default generators.

They also don’t allow the gathering of statistics and metrics using collect/2 and aggregate/2, so any validation and accounting that needs to be done will have to be done by hand, through regular output and other side effects.

Search macros

These limitations are due to an implementation detail of targeted properties. Targeted properties are in fact a special variation of a feature called search macros. There are two of them:

1. ?EXISTS(Var, Generator, Expression)has arguments that are similar to those in ?FORALL. However, this macro will succeed as soon as Expression returns true once, and will otherwise fail if it is allowed to run all of its executions while only returning false.
2. ?NOT_EXISTS(Var, Generator, Expression) is the opposite of ?EXISTS. It only succeeds if all executions run to completion while returning false.

Search macros allow us to add further search and validation to an existing property by embedding them inside the property. For example, if a company is doing video streaming or IoT data reporting, it may want to test a client that has multiple possible endpoints to contact based on arbitrary failures. In such a case, it may not just want a property that always passes, but one that just eventually works. It doesn’t matter if it fails fifty times, as long as at some point it does pass once.

We could, for example, illustrate the retry logic we just described with the following pseudocode:

prop_retry() ->
    ?FORALL({Data, Config}, {term(), environment_generator()},
    begin 
        cause_some_server_failures(Config), 
        ?EXISTS(IP, pick_server(Config),
            is_successful(request(IP, Data))) 
    end).

In this pseudocode, it doesn’t matter if all but one of the servers fail, as long as eventually the right server is picked and things pass.

Targeted properties were initially added to these search macros before being generalized with the ?FORALL_TARGETED mechanism. In fact, FORALL_TARGETED(Pattern, Generator, Property) is implemented roughly as ?NOT_EXISTS(Pattern, Generator, not(Property)).

Regardless of their limitations, targeted properties can prove to be very interesting and useful.