In a previous prost, I explained property based testing. In this post we’ll see a simple example in dotnet with Fscheck

Lets assume we built code to transfer money from account A to account B. Some properties that comes to mind are:

1. Successful transfer changes account balances.
2. Successful transfer leaves source balance as non-negative.
3. Failed transfer do not change account balances.

Our first implementation looks like this (don’t judge! … its supposed to be buggy)

class BuggyBank
{
    public int BalanceOfAccountA {get; set;} 
    public int BalanceOfAccountB {get; set;}
    
    public void TranserToAccountB(int Amount) 
    {
        BalanceOfAccountA -= Amount;
        BalanceOfAccountB += Amount;
    }
}

First we setup an empty dotnet unit test project like this:

mkdir FsCheckExample
cd FsCheckExample
dotnet new mstest
dotnet add package FsCheck --version 3.0.0-beta2

Then we add one test to validate all properties like this. Its vital to use QuickCheckThrowOnFailure() instead of QuickCheck() otherwise the test runner never reports failures.

    [TestMethod]
    public void MultiplePropertiesInOneTest()
    {
        Prop.ForAll<int, int, int>((StartBalanceForA, StartBalanceForB, AmountToTransfer) => {
            BuggyBank T = new()
            {
                BalanceOfAccountA = StartBalanceForA,
                BalanceOfAccountB = StartBalanceForB
            };
            try 
            {
                T.TranserToAccountB(AmountToTransfer);
            } 
            catch 
            {
                //The transfer failed
                bool BalancesUnchanged = (T.BalanceOfAccountA == StartBalanceForA && T.BalanceOfAccountB == StartBalanceForB);
                return BalancesUnchanged.Label("Failed transfer do not changes account balances.");
            }

            //Transfer succeeded
            bool BalancesChanged = T.BalanceOfAccountA != StartBalanceForA && T.BalanceOfAccountB != StartBalanceForB;
            bool NonNegativeBalanceOfA = T.BalanceOfAccountA >= 0;
            return
                NonNegativeBalanceOfA.Label("Successful transfer leaves source balance as non-negative")
                .And(BalancesChanged).Label("Successful transfer change account balances.")
            ;
            
        }).QuickCheckThrowOnFailure();
    }

When we run this test, FsCheck discovers the code allows transfers of 0 which violate the property that balances must change after successful transfer.

  Failed MultiplePropertiesInOneTest [674 ms]
  Error Message:
   Test method FsCheckExample.FsCheckExample.MultiplePropertiesInOneTest threw exception: 
System.Exception: Falsifiable, after 1 test (0 shrinks) (10302727913982160643,12688396740290863899)
Last step was invoked with size of 2 and seed of (10747404355721025928,11972757671557555113):
Label of failing property: Successful transfer change account balances.
Original:
(0, 0, 0)
with exception:
System.Exception: Expected true, got false.

After fixing that bug, FsCheck finds yet another bug! Transfers succeed even when the source account’s balance is insufficient:

  Failed MultiplePropertiesInOneTest [444 ms]
  Error Message:
   Test method FsCheckExample.FsCheckExample.MultiplePropertiesInOneTest threw exception:
System.Exception: Falsifiable, after 8 tests (4 shrinks) (16420426895032412258,4100991820053463935)
Last step was invoked with size of 9 and seed of (13117456436209885594,15897597155289983093):
Labels of failing property (one or more is failing):
Successful transfer change account balances.
Successful transfer leaves source balance as non-negative
Original:
(-2, -2, 2)
Shrunk:
(0, 0, 1)
with exception:
System.Exception: Expected true, got false.