Scala preconditions (assert, assume, require, ensuring)

Scala provides a set of preconditions functions (assert, assume, require, ensuring).

In addition to the actual functionality of dynamically check invariants, these functions are used for documentation and static code analysis.

These functions are used to do mainly Desing by Contract (DbC). It’s a software design technique which suggests that software designer should define formal, precise, and verifiable interface specifications for software components. Many programming languages have libraries for this purpose. Examples are: Java PBC, .NET Code Contracts and preconditions in Scala.

Let’s start with the similarities – all of these functions get an expression as a parameter and tests if it’s true.

So what is really the difference? (only in the intent expressed)

assert (java.lang.AssertionError) – a predicate which needs to be proven by a static code analyser to attempt to prove. It is something that you expect the static checker to be able to prove at compile time.

assume (java.lang.AssertionError) – an axiom for a static checker. It is something that the static checker can rely upon.

require (IllegalArgumentException) – Blames the caller of the method for violating the condition. Used as a pre-condition. ensuring is a post-condition.

Code samples of Scala preconditions

https://gist.github.com/maximn/9a56347c93eda5c508c0

Assert

val rnd = Math.random()
val n = Math.abs(rnd)
assert(n > 0)

Assume

val speedFromSensor: Double = ...
assume(speedFromSensor >= 0)

Rquire & Ensuring

def doublePositive(n: Int): Int = {
  require(n > 0)
  n * 2 // logic
} ensuring(n => n >= 0 && n % 2 == 0)
  • Note that assert & assume can be removed at compile time with the command line option to scalac : -Xdisable-assertions

More recommended reading –

Leave a Reply