The code as written could divide by zero. It may look like division by zero has been prevented, but there is a code path that fails. here it is again.

public decimal GrowthPercent(decimal ThisQuarterSales, decimal LastQuarterSales)
{
    if (LastQuarterSales == 0.0m && ThisQuarterSales == 0.0m)
    {
        // No sales means no growth.
        return 0.0m;
    }
    if (LastQuarterSales == 0.0m && ThisQuarterSales > 0.0m)
    {
        // Any sales over zero is interpreted as 100% growth.
        return 100.0m;
    }
    return (ThisQuarterSales / LastQuarterSales - 1.0m) * 100.0m;
}

If ThisQuarterSales is negative, the code falls through to the division. We want to prove that LastQuarterSales is not zero before we divide by it. We can do this using conditionals.

if (a)
    Assert(a);
else
    Assert(!a);

Think of the above code not as an algorithm that takes a single code path based on the value of “a”. Think of it as a logical statement. If A, then A. Otherwise, not A. It is obvious. And it can be applied to make the code obvious.

if (LastQuarterSales == 0.0m)
{
    Assert(LastQuarterSales == 0.0m);
    // ...
}
else
{
    Assert(LastQuarterSales != 0.0m);
    return (ThisQuarterSales / LastQuarterSales - 1.0m) * 100.0m;
}

With this form, we can assert that LastQuarterSales is not zero before we divide by it. The code will never throw. Q.E.D.

Let’s apply that form to the buggy code.

public decimal GrowthPercent(decimal ThisQuarterSales, decimal LastQuarterSales)
{
    if (LastQuarterSales == 0.0m)
    {
        Assert(LastQuarterSales == 0.0m);
        if (ThisQuarterSales == 0.0m)
        {
            // No sales means no growth.
            return 0.0m;
        }
        if (ThisQuarterSales > 0.0m)
        {
            // Any sales over zero is interpreted as 100% growth.
            return 100.0m;
        }
    }
    else
    {
        Assert(LastQuarterSales != 0.0m);
        return (ThisQuarterSales / LastQuarterSales - 1.0m) * 100.0m;
    }
}

The compiler will give you an error message. Not all code paths return a value. We can use the compiler’s inference engine to help us prove the correctness of our code. Change the conditions to ensure that all code paths return.

public decimal GrowthPercent(decimal ThisQuarterSales, decimal LastQuarterSales)
{
    if (LastQuarterSales == 0.0m)
    {
        Assert(LastQuarterSales == 0.0m);
        if (ThisQuarterSales <= 0.0m)
        {
            // No sales means no growth.
            return 0.0m;
        }
        else
        {
            // Any sales over zero is interpreted as 100% growth.
            return 100.0m;
        }
    }
    else
    {
        Assert(LastQuarterSales != 0.0m);
        return (ThisQuarterSales / LastQuarterSales - 1.0m) * 100.0m;
    }
}

By putting the division inside of an else, we’ve proven that it will not divide by zero. At that point, the compiler was able to help us find the code path that would otherwise have caused the bug. We fixed the bug, and the compiler helped us prove that it was fixed.