API Discussion: Specifying and Validating Properties

[jlink]

Other than Jqwik 1, which went with a JUnit Platform engine from day one, Jqwik 2's core will consist of a plain programming API for specifying and validating properties. The engine will be tackled in a different module.

API Suggestion

Simple Property Check

The simples invariant is if the code under test returns true (valid) or false (invalid):

PropertyDescription property =
	PropertyDescription.property()
		   .forAll(Numbers.integers().between(0, 100))
		   .check(i -> i >= 0 && i <= 100);

PropertyValidator validator = PropertyValidator.forProperty(property);
PropertyValidationResult result = validator.validate();

Simple Property Assertions

Alternatively invariants can be formulated by standard assertions, e.g. through AssertJ:

PropertyDescription property =
	PropertyDescription.property()
		   .forAll(Numbers.integers().between(0, 100))
		   .verify(i ->  {
			   assertThat(i).isBetween(0, 100);
		   });

PropertyValidator validator = PropertyValidator.forProperty(property);
PropertyValidationResult result = validator.validate();

Property Validation with different validation Strategy

The strategy to validate a given property can vary a lot and across different axes.
Some examples of variation:

• Run 1000 purely randomized samples
• Run with as many samples as you can in 5 seconds
• Run exhaustively, i.e. all possible value combinations
• Run all tries in parallel using virtual threads

PropertyDescription property = ...
PropertyValidator validator = PropertyValidator.forProperty(property);

PropertyValidationStrategy strategy =
	PropertyValidationStrategy.builder()
				  .withMaxRuntime(Duration.ofSeconds(5))
				  .withGeneration(PropertyValidationStrategy.GenerationMode.EXHAUSTIVE)
				  .withConcurrency(ConcurrencyMode.VIRTUAL_THREADS)
				  .build();
PropertyValidationResult result = validator.validate(strategy);

Property Description with Additional Assumption

Some preconditions cannot be put into the arbitraries and require a value-spanning assumption.

var property = PropertyDescription.property()
		   .forAll(Numbers.integers(), Numbers.integers())
		   .check((i1, i2) -> {
		       Assume.that(i1 < i2);
		       return (i2 - i1) > 0
		   });

PropertyValidationResult result = PropertyValidator.forProperty(property).validate();

Statistical Validation

Statistical validation is crucial when dealing with not fully deterministic algorithms;
ML classification is a typical example.

PropertyDescription property = ...
PropertyValidator validator = PropertyValidator.forProperty(property);

PropertyValidationResult result = validateStatistically(93.0);

Rationale(s)

Split property description from validation

Validation could automatically start with the check(..) or verify(..) method,
thereby saving the user the effort of creating a validator object and running validate(..).
This would be closer to how other PBT libraries do it.

It would, however, make two things more difficult:

• Getting hold of the object describing the property
• Applying different validation strategies

A convenience method like validateAtOnce(..) could be added later to make the simplest case simpler.

Why not Calling the interface PropertyDescription just Property

Property is the name for the Jqwik 1 main annotation.
I'd like to keep the name available for Jqwik 2's engine annotations without having to rely on package names.

Why not using an additional spec method for Assumptions?

Assume.that(..) will throw a TestAbortedException.
This approach allows to fail an assumption at any time during property validation.
Moreover, an additional assume(..) method when building the property description would have to get the
same parameters as the check or verify method, leading to unnecessary code duplication.

Open Questions

• Would PropertySpecification be a more exact name than PropertyDescription?
• Instead of having a validateStatistically(..) method there could be a StatisticalValidator type.
• Instead of starting a fluent API with PropertyDescription.property() there could be an explicit property builder class.