在Scala中，假设（assumption）和断言（assertion）有何含义区别？

Question

Scala似乎定义了3种断言：assert，require和assume。

据我理解，与通用断言相比，require的差异在于它专门用于检查输入（参数、传入的消息等）。那么assume有什么含义呢？

- Ivan

---

http://www.maxondev.com/scala-preconditions-assert-assume-require-ensuring/ - Maxim

Answer 1

如果您查看Predef.scala中的代码，您会发现这三个函数都执行非常相似的工作：

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") 
} 

还有一些版本接受额外的参数用于报告目的(请参见http://harrah.github.com/browse/samples/library/scala/Predef.scala.html)。

它们的区别在于抛出的异常类型和生成的错误消息。

但是，静态检查器可能会对它们进行不同的处理。 assert的意图是指定一个条件，静态检查应该尝试证明它成立，assume用于一个假设检查器可以假定为真的条件，而require则指定了调用方必须确保的条件。如果静态检查器发现assert存在违规情况，它将视其为代码中的错误，而当require被违反时，则认为调用方是有问题的。

- Adam Zalcman

---

有使用静态检查器的吗？我希望有，看起来很酷 :-) - Ivan

我之前听说过一个，最近找到了这个链接：https://github.com/alacscala/alacs#readme，但看起来他们已经停止更新了。不幸的是，维基百科上的文章http://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis没有Scala的相关条目。 - Adam Zalcman

Answer 2

区别

assert()和assume()的区别在于：

• assert()是一种记录并动态检查不变量的方式，
• 而assume()旨在供静态分析工具使用。

assert()的预期用户/上下文是测试，如Scala JUnit测试，而assume()的预期用户/上下文是“作为函数前置条件和后置条件的设计契约样式规范的一种手段，意图使这些规范可以被静态分析工具消耗”（摘自scaladoc）。

静态分析/模型检查

在静态分析的背景下，如Adam Zalcman所指出的，assert()是一个全执行路径断言，用于检查全局不变量，而assume()则在本地起作用，以减少分析器需要进行的检查量。 assume()在假设-保证推理的上下文中使用，这是一种分治机制，帮助模型检查器假定关于方法的某些内容，以解决当尝试检查程序可能采取的所有路径时出现的状态爆炸问题。例如，如果您知道在程序的设计中，函数f1(n1：Int，n2：Int)永远不会传递n2 < n1，那么明确说明这个假设将有助于分析器不必检查大量的n1和n2组合。

实践中

在实践中，由于此类整体程序模型检查器仍然主要是理论，让我们看看scala编译器和解释器的行为：

1. 在运行时都会检查assume()和assert()表达式
2. -Xdisable-assertions禁用了assume()和assert()的检查

更多

关于此主题的更多信息，请参阅出色的scaladoc：

断言

提供了一组assert函数，可用作记录并动态检查代码中的不变量的方法。提供了针对与静态分析工具一起使用的assert变体：assume、require和ensuring。 require和ensuring旨在用作函数的前置条件和后置条件的设计契约样式规范，以消耗静态分析工具。例如，

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

addNaturals函数的声明表示传递的整数列表应该只包含自然数（即非负数），并且返回的结果也将是自然数。require与assert不同之处在于，如果条件失败，则函数的调用者应承担责任，而不是在addNaturals本身中产生逻辑错误。ensures是一种断言形式，它声明了函数关于其返回值提供的保证。

- vijucat

Answer 3

我支持Adams的回答，以下是一些小的补充：

当 assume 被违反时，验证工具会默默地删减路径，即不再深入跟踪该路径。

因此，assume 经常用于制定前置条件，assert 用于制定后置条件。

许多工具使用这些概念，例如共模测试工具 KLEE，软件有界模型检查工具如 CBMC 和 LLBMC，以及部分基于抽象解释的静态代码分析工具。文章 Finding common ground: Choose, Assert, Assume 介绍了这些概念并试图将它们标准化。

- DaveFar