[ANN] PropCheck.jl

PropCheck.jl

Hello everyone! After more than 4 years of WIP development, I’m very excited to announce PropCheck.jl, a property based testing framework loosely inspired by QuickCheck & Hedgehog. It features type based generation, composition of generators, map/filter of generated instances and automatic test-case shrinking/minimization. There are quite a lot of planned features, so please do check out the documentation! Some of these are quite a bit harder to do than others, so please be patient with me :slight_smile: Contributions are always welcome though - I hope the internals are clear enough, though some parts definitely need more devdocs :sweat_smile:

A very early version of this package was used in the past to find an unreachable reached catastrophic failure in Julia itself!

Due to the time already spent on developing this package, the currently latest version is 0.9.2, supporting Julia versions 1.6 and newer.

FAQ

What is property based testing?

In a nutshell, property based testing means thinking about the (mathematical) properties you as a developer would like your code to have, and then testing/checking in some way whether these properties hold. This needn’t be exhaustive - just for +(::Int64, Int64) there are already 2^128 possible input bitpatterns, too many to practically check completely. In a sense, property based testing as employed by PropCheck.jl is a form of fuzzing.

Why property based testing?

Aren’t unit tests sufficient? Well… No! If you can’t be sure that your code obeys the properties you would like it to have, you can get disastrously wrong results. In the worst case, you can end up drawing wrong conclusions from your scientific models, or crash your server in production due to a faulty assumption.

Not knowing about the desired properties & testing for them can lead to things like this - quoting Hillel Wayne (who specializes in formal methods):

In 2010 Carmen Reinhart and Kenneth Rogoff published Growth in a Time of Debt. It’s arguably one of the most influential economics papers of the decade, convincing the IMF to push austerity measures in the European debt crisis. It was a very, very big deal.

In 2013 they shared their code with another team, who quickly found a bug. Once corrected, the results disappeared.

Greece took on austerity because of a software bug. That’s pretty fucked up.

(This quote is from his article How do we trust science code?)

For a basic introduction to property based testing and how it relates to Julia in particular, please check out this section in the docs!

What about formal specifications?

While efforts regarding formal specifications & machine checkable proofs are comendable, I think we can get quite far with property based testing & fuzzing before we need to tackle the dragon that is formal methods & verification. PropCheck.jl is decidedly not in the formal verification camp - it’s not an interface to SAT or SMT solvers, but a fuzzer. Said differently, property based testing + fuzzing are a fuzzy, statistical subset of full formal verification. You can think of running fuzzing tests as increasing confidence in the correctness of your code each time you run your testsuite, due to different inputs being chosen.

That being said, if this package becomes obsolete due to tremendous advances in formal methods & verification in Julia, I’ll happily retire this package to the annals of history :slight_smile:

What about package XYZ?

There are a number of other codebases related to property based testing (for example, JCheck.jl, QuickCheck.jl or RandomizedPropertyTest.jl) but to my eyes, they are either very old (10+ years!) and don’t support modern Julia, don’t support shrinking or don’t really compose their generators well, due to being based on QuickCheck. PropCheck.jl, while certainly taking inspiration from QuickCheck, is using a mixed approach, focusing on integrated shrinking. This has advantages and disadvantages, but from my experience with the package so far, the current architecture is pretty extensible and works much better than a plain implementation of QuickCheck (Julia is much less focused on types than Haskell is, after all; much of the information we have about a type is implicit & not guaranteed, and even with that, some type based shrinks are just plain bad, due to even their types not capturing the full semantics of the produced values). Most of the features currently in PropCheck.jl came about because I ran into an issue that I wanted to solve when testing a different codebase - hence, the package is already at 0.9.1 :slight_smile:


One issue with developing a package in private for such a long time is that it can happen that I’m missing an obvious use/fatal error case that I just didn’t think about/haven’t encountered due to knowing the “happy path” of the package, so to speak - so please do give the package a try and report errors, bugs & feature requests at the issue tracker!

Finally, I’d like to thank the fine folks at the JuliaLang Zulip, in particular @Mason, @jakobnissen, jar and Michael Fiano (not sure about the discourse names, sorry!) for giving the first draft of the documentation a good look-over and spotting some issues :slight_smile:

46 Likes

I am eager to start using this tool – I have wanted a quickcheck-like tool in julia for a while.

Could you consider making an “official” badge for it so that my repositories can proudly announce they are being tested in this fashion? And so that we can advertise and popularize PropCheck. Similar to JET and Aqua:

JET static analysis

Aqua QA

I personally like the JET one better.

4 Likes

I’m looking forward to your feedback!

Oh dear - I haven’t thought about that at all :sweat_smile: I’m afraid there isn’t as pretty a logo as for JET.jl (yet?), so this will have to wait a bit - sorry! Happy to take suggestions though :slight_smile:

1 Like

Something, something, propeller with Julia colors

7 Likes

Funny thing is, the “JET logo” is just the standard unicode emoji for a plane as discussed here: Logo or Readme badge similar to Aqua's · Issue #375 · aviatesk/JET.jl · GitHub (It is not official, it is just what I was able to make with minimal effort). Kinda like this

4 Likes

Yes, I tried fiddling with the shields.io link a bit once I saw how it works :slight_smile: Trouble is, “PropCheck” is quite a bit more abstract than “JET”, so there isn’t a direct emoji to use.

I quite like the idea with props in different colors; I hadn’t noticed that it could be read like that too! Perhaps a logo in some form of schematic or blueprint, to tie it to the “check properties” theme?

Pretty common for boat and airplane propellers to have 3 blades. Wonder if you could take a simple looking one and make each blade one of the Julia colors (so that it looks like the 3 dots logo)?

1 Like

I took a crack at a propeller logo. But I’m not graphic designer if someone wants to improve it!

I couldn’t find documentation about the color codes for the Julia dots. If someone could point me to that, I’d appreciate it!

1 Like

@cormullion

I’ve read through some of the documentation, and I am really loving this idea! I always feel disgusted by my test blocks looking like this:

@testset "equality" for x in rand(10)
    @test f(x) == g(x)
end

I’ll try to integrate it into my projects and see how I go.

1 Like

Is something like this what you’re looking for?

http://juliagraphics.github.io/Colors.jl/stable/namedcolors/#Colors.JULIA_LOGO_COLORS

2 Likes

Nice!

Colours are in Colors.jl as Colors.JULIA_LOGO_COLORS, - Named Colors · Colors

2 Likes

Brilliant!

29 Likes

Amazing!!

1 Like

After some (surprisingly little) work, I’ve just released 0.9.2 - which now supports Julia version 1.6 and up :slight_smile: This should make it possible to integrate PropCheck.jl into existing testsuites with relative ease, without having to make special considerations regarding LTS or such.

1 Like

If we’re going for propeller designs for the logo, it would be cool to use a toroidal propeller, which both look a bit more like the Julia logo (from top down), and are considered significant upgrades to traditional propellers in noise pollution.

I realise that this adds nothing to the discussion given that Rafael has already made a great logo :stuck_out_tongue:

4 Likes

I don’t know, mentioning technology that represents a significant improvement even though everyone has already decided to go another direction is kinda on brand for Julians :wink:

6 Likes

One toroidal version:

14 Likes

A usage question:

For some of the types in a library of mine I already have uniform random samplers. Should I use them to create PropCheck.generate methods or should I only rely on map/filter/interleave?

1 Like