与断言相比,scala中的假设是什么意思？

Question

斯卡拉似乎定义3个两种断言:assert,require和assume.

据我所知,差异(与通用断言相比)require是它专门用于检查输入(参数,传入消息等).那么什么意思assume呢？

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违反时它会假定调用者有错.

Answer 2

区别

assert()和assume()之间的区别在于

• assert()是一种记录和动态检查不变量的方法
• assume()旨在被静态分析工具使用

assert()的目标消费者/上下文是测试,例如Scala JUnit测试,而assume()的消费者/上下文是"作为函数的前后条件的合同样式规范的一种手段,其中意图是静态分析工具可以使用这些规范"(摘自scaladoc).

静态分析/模型检查

在静态分析的上下文中,正如Adam Zalcman指出的那样,assert()是一个全执行路径断言,用于检查全局不变量,而assume()在本地工作以减少分析器需要的检查量.做.假设()用于假设保证推理的上下文,这是一种分而治之的机制,可以帮助模型检查员假设某些方法,以便解决当试图检查程序的所有路径时出现的状态爆炸问题可能需要.例如,如果你知道在你的程序设计中,函数f1(n1:Int,n2:Int)永远不会传递n2 <n1,那么明确地说明这个假设将有助于分析器不必检查很多组合n1和n2.

在实践中

在实践中,由于这样的整个程序模型检查器仍然主要是理论,让我们看一下scala编译器和解释器的作用:

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

更多

更多关于这个主题的优秀scaladoc:

断言

提供了一组assert函数,用作记录和动态检查代码中不变量的方法.通过向命令提供命令行参数-Xdisable-assertions,可以在运行时省略断言语句scala.

变体assert还提供用于静态分析工具使用:assume,require和ensuring.require并且确保旨在用作功能的前后条件的合同样式规范的手段,意图是静态分析工具可以使用这些规范.例如,

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

addNaturals的声明声明传递的整数列表应该只包含自然数(即非负数),并且返回的结果也是自然的.require与assert的区别在于,如果条件失败,那么函数的调用者应该责备而不是在addNaturals本身内做出的逻辑错误.确保是一种断言形式,声明函数提供的关于它的返回值的保证.)

Answer 3

我是亚当斯的第二个回答,这里只是一些小补充:

当assume违反时,验证工具会默默地修剪路径,即不会更深入地跟踪路径.

因此assume通常用于制定前提条件,assert以制定后置条件.

许多工具都使用这些概念,例如,模仿测试工具KLEE,软件界限模型检查工具(如CBMC和LLBMC),部分还通过基于抽象解释的静态代码分析工具.文章寻找共同点:选择,断言,假设介绍了这些概念并尝试对它们进行标准化.