What is a property?
10 points by ugur
10 points by ugur
We can find Hoare logic here. Let pre and post be pre- and postconditions respectively for an arbitrary pure function f. Specifically,
f :: a -> b
pre :: a -> Bool
post :: b -> Bool
Also, let's generalize the pattern in the article where we put an implied precondition before the rest of the program:
type Property a = a -> Bool
(===>) :: Property a -> Property a -> Property a
p ===> q = \a -> p a `implies` q a
And now we can say that the triple (pre, f, post) is valid whenever the following composite is constantly true:
pre ===> post . f
This ought to give a comma category of triples with types given by f, but I haven't fully worked it out. (Obviously this can't be done over classic Hask).
Author here, indeed, in more imperative languages, PBT looks a lot more like Hoare-style reasoning with explicit assume and assert calls. We would even be able to switch between random testing and hoare logic verification for the same program.
The categorical way I would think of Hoare triples is (bi)fibrations:
t -> Bool form a category of subsets/predicates over the base category, where morphisms are implication arrowsp that sends t -> Bool (the subsets over t) to t is a bifibration(pre, f, post) is valid is an arrow alpha : pre -> post over f (that is, p(alpha) = f).Precisely this example is worked out in more details in Functors are type refinement systems, Melliès and Zeilberger, 2015.
Could proptest be adapted to use this approach?
proptest! {
#[test]
fn my_test(x in my_actual_property()) {
// Where x is of type TestCaseResult, and my_actual_property returns a impl Strategy<Value=TestCaseResult>
return x;
}
}
Certainly rust lacks do notation, so it might be annoying to write, but at least Strategy is a monad.
You can almost certainly build a property runner that could accommodate this. I haven’t read proptest internals before, so I’m not sure how that would work, but I presume it actually shouldn’t be that hard.
The back-and-forth between generators and properties reminds me of another approach to randomized testing: rather than creating a random artefact and verifying that a property holds, instead create a random list of operations and when applying the operations verify that the invariants continue to hold. Previously.