Scala - Design by Contract

Design by Contract

Design by Contract (DbC) (aka Programming by Contract) is an approach to developing and engineering software. With Design by Contract programmers should define formal specifications for modules, and those specifications are called contracts. There are basically three types of contracts.

• Preconditions - requirements for the module to run correctly (must be true before it is invoked)
• Postconditions - the results that the module guarantees (must be true after it is invoked)
• Invariants - these conditions must be true before and after the module runs

In other words, preconditions are asking yourself - what does my module expect?
Postconditions - what does my module guarantee?
Invariants - what does my module maintain?

Because you guarantee certain conditions to be true as long as your requirements are satisfied - it is a very formal way of designing software and may help you write formal proofs of correctness for your software using for instance Hoare logic - would you believe?

But seriously, the technique can prove very useful and promises making debugging to be a lot easier, due to the fail-hard principle which means that if the preconditions are not met (i.e. any of them isn't) - it all crashes, perhaps with a big boom, but providing the developer with useful information regarding the failure.

Design by Contract is a bit similar to defensive programming, but it differs in that the module is not responsible for figuring out what went wrong and why - it just fails when the preconditions are not met (which is probably a bit easier). Enough introduction.

Design by Contract in Scala - precondition

Although Scala does not provide support for Design by Contract as such, we can still implement it without having to use any external libraries and in quite an elegant fashion.

Let's not wait any longer and see some code!

package me.m1key.dbc

class Account(b: Int) {
    
    private var balance = b
    
    printf("Creating a new account with balance: %d\n", balance)
    
    require(balance >= 0.0, "Balance must be > 0 and is: %d".format(balance))
    
    
    def debit(amount: Int) = {
        printf("Debitting: %d ", amount)
        balance -= amount
        printf(", balance: %d\n", balance)
    }
    
    def credit(amount: Int) = {
        printf("Adding credit: %d ", amount)
        balance += amount
        printf(", balance: %d\n", balance)
    }

}

Here we can see a simple Account class that you create by providing it an initial amount (b: Int). Because I did not use val/var keywords, this field is not accessible from the outside, which is good as we don't want anyone messing around with the balance in ways other than the debit/credit methods.

The code below class declaration but above the methods - we assign the initial value to a private variable balance. It is not accessible from the outside world. It will hold the actual balance that we will modify (b: Int is a val, we cannot change its value).

The next two lines (printf and require) are what you would call constructor code in Java. Printf just prints some useful info to the console (for the example sake), and then - please welcome the require method of the Scala Predef object which is automatically imported by the compiler for you convenience. The Predef object defines or imports items like String (the Scala version), collections, exceptions, Pair, Triple and more useful stuff.

Now, what the require method does here is it makes sure that balance is greater than or equal 0. Otherwise - fail hard, you get an exception:

val account11 = new Account(-1) // Error

Creating a new account with balance: -1
Exception in thread "main" java.lang.IllegalArgumentException: requirement failed: Balance must be > 0 and is: -1
    at scala.Predef$.require(Predef.scala:117)
    at me.m1key.dbc.Account.<init>(Account.scala:9)
    at me.m1key.dbc.Launch$.main(Launch.scala:11)
    at me.m1key.dbc.Launch.main(Launch.scala)

We only make the check when the object is created, thus this is a precondition. At this point, you can further modify the balance and set it to negative numbers without any exceptions - which we shall fix. By the way, you can put the require method anywhere you want, not just in this particular place.

Note - why use Int for representing money and not double?

Good question. To find out, look at this code and compare what you think it should return with what it actually does (you're going to have to run it yourself).

def x: Double = 2.00
        def y: Double = 1.90
        println(x - y)

Design by Contract in Scala - postcondition

Let us fix this problem. Let us add a postcondition that will verify the balance to be debited.

def debit(amount: Int) = {
        printf("Debitting: %d ", amount)
        assume(balance - amount >= 0.0, "This debit amount exceeds current balance: %d".format(amount))
        balance -= amount
        printf(", balance: %d\n", balance)
    }

Here we check whether the balance stays above or at 0 before we even subtract.

Note that we used assume and not require like we did for the precondition. These two methods are basically the same except that assume throws an AssertionError while require throws an IllegalArgumentException. Therefore assume is more natural for postconditions while require is more natural for preconditions.

Drawbacks

The drawback is that there is no way to disable these checks - if you don't comment them out, they will stay and run in production code.
Update 2010-02-13: As duyn kindly pointed out, this is not entirely true. As of Scala 2.8 the elidable annotation is available and it means that whatever is annotated with it - can be removed from the compiled code (with a command similar to scalac -Xelide-methods-below=1000; I got it from Scala docs). And, the assume method is indeed annotated with it, so it can be disabled for production code (as well as the assert method). However, the require method is not annotated, which means it stays in the code unless you comment it out.
Thanks duyn for your helpful remark!

Now, like I previously said, the require method stays in the code. This may not be acceptable for performance reasons, but also you may not like your code to fail-hard. You might be developing a service that should just run (for example, see Scala Actors).

The two methods - assume and require are very simple. Their limitation is that they only accept simple expressions. So, if you are looking for more flexibility, you may look at the Ensuring class (it accepts functions as predicates).

Conclusion

Design by Contract is an interesting approach, however it has pretty much been replaced these days by Test Driven Development and probably for good reasons (TDD is said to be more flexible and natural). On the other hand, an important thing to notice is that TDD and DbC are not necessarily mutually exclusive, so you might as well try using a combination of both.

Download source code for this article

PS. You can find an interesting way of implementing DbC in Scala on this Scala Wiki page.