Ironing out bugs with FsCheck

🗒️ You can read the source code for this article.

During this week, I was tasked to write some property-based tests to a slightly critical portion of our system that handles financial transactions. You won’t see the exact same tests I wrote at work due to legal reasons1. Instead, a buggy fictional scenario with similar code structure will be used.

Our codebase is written in F#, and luckily, there’s an amazing library called FsCheck that can be used for this purpose. But… What is property-based testing? According to FsCheck’s documentation:

The programmer provides a specification of the program, in the form of properties which functions, methods or objects should satisfy, and FsCheck then tests that the properties hold in a large number of randomly generated cases. While writing the properties, you are actually writing a testable specification of your program.

In short, property-based testing is about writing an specification of your code through expected output characteristics. Scott Wlaschin wrote an awesome article about common properties found on code.

While breaking the code apart, I noticed that the first testable property was applicable to the section “Different paths, same destination”. Before starting, load the needed dependencies for our testing:

#r "nuget: FsCheck, 2.16.5"

open FsCheck
open System

Picture the following scenario, you have two lands and you have to sum the area of both. The sum cannot output a negative number. This is quite easy, isn’t it? How hard can it be to introduce a bug?

type Land =
    { Width: float; Height: float }

module Land =
    let area value = value.Width * value.Height
    let sumAreas a b = area a + area b

Executing the code shows us that our implementation is correct according to the business rule:

let store = { Width = 10; Height = 45 }
let factory = { Width = 5; Height = 10 }

Land.sumAreas store factory // 500.0

But… is it, really? Let’s bring FsCheck to the game and write a simple test for the associative property:

let ``associativity of land sums`` (landOne, landTwo) =
    let a = Land.sumAreas landOne landTwo
    let b = Land.sumAreas landTwo landOne
    b = a

let ``sum of land areas is always positive`` (landOne, landTwo) =
    (Land.sumAreas landOne landTwo) > 0

A bit weird, isn’t it? In F#, you can use backticks around a string to make it a valid identifier. In this case, associativity of land sums is just as valid as AssociativityOfLandSums, just easier to read.

This function takes a tuple with two values: landOne and landTwo. Thanks to F#’s type inference, there’s no need to explicitly declare their types, as they are being inferred by their usage in the sumAreas function that only takes arguments of the type Land.

The test consists in getting the output of sumAreas with reversed parameters and comparing to see if the argument order changes the output. Which shouldn’t. Let’s feed FsCheck this function and see what happens:

Check.Quick ``associativity of land sums``
Falsifiable, after 1 test (0 shrinks) (StdGen (511870660, 297192323)):
{ Width = -0.0
  Height = -0.0 }
{ Width = nan
  Height = 0.0 }
val it: unit = ()

Bingo! We already found a runtime bug! If one of the values is Nan, our software does not conform to the specification2. There are a multitude of ways to solve this. Some examples are: treating this individually at the area function or treating both values at the same time on the sumAreas function.

Again, thankfully, Scott Wlaschin has also covered this up on “Creating modules for wrapper types”. You can imagine it as a constructor based on the module system, it’s really neat! However, it’s impossible to apply this here as signature files are not available on F# scripts. Here’s a quick glance on how the create function could look like:

    let create width height =
        let isValid x =
            if Double.IsNaN(x) || Double.IsInfinity(x) || Double.IsNegative(x)
            then None
            else Some x

        let width = isValid width
        let height = isValid height

        match (width, height) with
        | (Some width, Some height) ->
            Ok { Width = width; Height = height }
        | _ -> Error "Invalid measurements"

Alright, we know how to fix our code but we are unable to implement it on our script file… Writing a custom Generator that only spits valid data is an alternative. Again, there are numerous ways to implement a generator, and I have opted for the gen computation expression approach.

let validLandGenerator =
    gen {
        let biggerOrEqualToZero = Gen.filter (fun (x: NormalFloat) -> x.Get >= 0.0)
        let! width = Arb.generate<NormalFloat> |> biggerOrEqualToZero
        let! height = Arb.generate<NormalFloat> |> biggerOrEqualToZero

        return { Width = width.Get; Height = height.Get }

What’s NormalFloat? The documentation states: “Represents a float that is not NaN or Infinity.”. This is perfect! Then we pipe the Generator to our function biggerOrEqualToZero to make sure we don’t get negative numbers.

Here comes a really good tip. At work we struggled with functions taking two custom generators, we just couldn’t figure it out how to pass them. Well, we struggled so you don’t need to:

let twoValidLandsGenerator =
    Gen.map2 (fun landOne landTwo -> (landOne, landTwo)) validLandGenerator validLandGenerator
    |> Arb.fromGen

Now testing our two properties is trivial:

Check.Quick (Prop.forAll twoValidLandsGenerator ``associativity of land sums``)
Check.Quick (Prop.forAll twoValidLandsGenerator ``sum of land areas is always positive``)

  1. I don’t have a lawyer. ↩︎

  2. Which just expects the sum of the areas. 😁 ↩︎

Articles from blogs I follow around the net

The four tenets of SOA revisited

Twenty years after. In the January 2004 issue of MSDN Magazine you can find an article by Don Box titled A Guide to Developing and Running Connected Systems with Indigo. Buried within the (now dated) discussion of the technology…

via ploeh blog March 4, 2024

Building a demo of the Bleichenbacher RSA attack in Rust

Recently while reading Real-World Cryptography, I got nerd sniped1 by the mention of Bleichenbacher's attack on RSA. This is cool, how does it work? I had to understand, and to understand something, I usually have to build it. Well, friends, that is what…

via blog March 4, 2024

How to unbreak Dolphin on SteamOS after the QT6 update

A recent update to Dolphin made it switch to QT6. This makes it crash with this error or something like it: dolphin-emu: symbol lookup error: dolphin-emu: undefined symbol: _Zls6QDebugRK11QDockWidget, version Qt_6 This is fix…

via Xe Iaso's blog March 3, 2024

Generated by openring