What is the meaning of an assumption in scala compared to an assertion?

Scala seems to define 3 kinds of assertions: assert, require and assume.

As far as I can understand, the difference (compared to a generic assertion) of require is that it is specifically meant for checking inputs (arguments, incoming messages etc). And what's the meaning of assume then?

Solution 1:

If you look at the code in Predef.scala you'll see that all three do very similar job:

def assert(assertion: Boolean) { 
  if (!assertion) 
    throw new java.lang.AssertionError("assertion failed") 
} 

def assume(assumption: Boolean) { 
  if (!assumption) 
    throw new java.lang.AssertionError("assumption failed") 
} 

def require(requirement: Boolean) { 
  if (!requirement) 
    throw new IllegalArgumentException("requirement failed") 
} 

There are also versions which take extra arguments for reporting purposes (see http://harrah.github.com/browse/samples/library/scala/Predef.scala.html).

The difference is in the exception type they throw and error message they generate.

However, static checkers could treat all three differently. The intention is for assert to specify a condition that a static check should attempt to prove, assume is to be used for a condition that the checker may assume to hold, while require specifies a condition that the caller must ensure. If a static checker finds a violation of assert it considers it an error in the code, while when require is violated it assumes the caller is at fault.

Solution 2:

The difference

The difference between assert() and assume() is that

• assert() is a way to document and dynamically check invariants, while
• assume() is intended to be consumed by static analysis tools

The intended consumer / context of assert() is testing, such as a Scala JUnit test, while that of assume() is "as a means of design-by-contract style specification of pre- and post-conditions on functions, with the intention that these specifications could be consumed by a static analysis tool" (excerpted from the scaladoc).

Static analysis / model checking

In the context of static analysis, as Adam Zalcman has pointed out, assert() is an all-execution-paths assertion, to check a global invariant, while assume() works locally to pare down the amount of checking that the analyzer needs to do. assume() is used in the context of assume-guarantee reasoning, which is a divide and conquer mechanism to help model checkers assume something about the method so as to tackle the state explosion problem that arises when one attempts to check all paths that the program may take. For example, if you knew that in the design of your program, a function f1(n1 : Int, n2:Int) is NEVER passed n2 < n1, then stating this assumption explicitly would help the analyzer not have to check a LOT of combinations of n1 and n2.

In practice

In practice, since such whole-program model checkers are still mostly theory, let's look at what the scala compiler and interpreter does:

1. both assume() and assert() expressions are checked at runtime
2. -Xdisable-assertions disables both assume() and assert() checking

More

More from the excellent scaladoc on this topic:

Assertions

A set of assert functions are provided for use as a way to document and dynamically check invariants in code. assert statements can be elided at runtime by providing the command line argument -Xdisable-assertions to the scala command.

Variants of assert intended for use with static analysis tools are also provided: assume, require and ensuring. require and ensuring are intended for use as a means of design-by-contract style specification of pre- and post-conditions on functions, with the intention that these specifications could be consumed by a static analysis tool. For instance,

def addNaturals(nats: List[Int]): Int = {
  require(nats forall (_ >= 0), "List contains negative numbers")
  nats.foldLeft(0)(_ + _)
} ensuring(_ >= 0)

The declaration of addNaturals states that the list of integers passed should only contain natural numbers (i.e. non-negative), and that the result returned will also be natural. require is distinct from assert in that if the condition fails, then the caller of the function is to blame rather than a logical error having been made within addNaturals itself. ensures is a form of assert that declares the guarantee the function is providing with regards to it's return value. )

Solution 3:

I second Adams answer, here are just some small additions:

When assume is violated, the verification tool silently prunes the path, i.e. does not follow the path any deeper.

Hence assume is often used to formulate pre-conditions, assert to formulate post-conditions.

These concepts are used by many tools, e.g. the concolic testing tool KLEE, software bounded model checking tools like CBMC and LLBMC, and partly also by static code analysis tools based on abstract interpretation. The article Finding common ground: Choose, Assert, Assume introduces these concepts and tries to standardize them.