Design by Contract: Motivation

Design-by-contract is a tool that is extremely useful for everyday development and debugging. This section will show with a simple example how severe bugs could have been found and fixed early if the requirements and desired guarantees of a routine would have been specified early on.

Example: Square Root Function

Simple Implementation

Consider the following implementation of a square root function using a loop. It starts by setting r to 1 in the first iteration and to the mean of last and a / last in the following iterations. The loop terminates when r stops changing:

Finding Bugs

Let's play around with some more values passed to sqrt:

We found a problem. Passing -16 causes the loop to run forever, no result is produced. This is not surprising because there is no proper definition of an integer valued square root of a negative number, so this case should be forbidden.

In other languages, we would add checks like an assert. But this would lead to an error in our code of sqrt, which is misleading since the error is actually in the caller that passes an invalid argument value to a call to sqrt. Better would be something like throwing an exception that explains that we received an invalid argument. But then still, the exception code would be somewhere in the implementation of the routine, instead of part of its specification like the type signature.

Preconditions

In Fuzion, conditions that must hold for a feature call to be valid can be formally specified in a precondition that is part of the feature's signature. In our case, we add the precondition a >= 0 to document and enforce that the argument is never negative:

When running this code now, we see a runtime error at the failing precondition together with a stack trace that shows the call chain.

Unlike languages with exception handling, Fuzion does not permit using failed runtime checks for control flow. There is no way a thread could catch the error and continue as if everything was fine. A failed precondition means that there is a serious bug in the program that caused an unexpected error. The data that was currently processed is hence in an inconsistent state. Instead, the current thread will be terminated and all its local data will be deleted.

Back to the square root example, we can remove the failing call and continue testing:

Now, we see another precondition failure, but this time it is not the precondition of sqrt that fails, but the precondition of the division i32.infix / fails for the case test(0). This means we have a bug in the code:

We did not consider that r could become 0 such that a / last results in a division by zero. This time, the failure is not the caller's fault. Our implementation is to blame and needs to be fixed:

More bugs

It often helps to test with extreme values, so let's continue testing with large values:

We see another problem here. Our sqrt function suddenly returns a negative value when calling it on 2147483647. We do not want any negative values as the result here. We should have added proper checks to catch wrong results!

Postconditions

Postconditions are Fuzion's means to formally describe the guarantees given by a feature once it returns to the caller. In our example, we can use postconditions to document that the result should be a positive integer whose square is <= a while the next bigger integer's square would be larger than a. The following updated example includes a postcondition that checks that these conditions hold for the result:

Running this example now traps the negative result in the postcondition, which shows that we have a bug in our implementation of sqrt. The problem is an integer overflow in last + a / last. Using the saturating plus +^ instead of the normal + solves this: