leon -xlang的短路评估

Question

考虑以下否定布尔值的复杂方法(取决于短路评估)：

def negate(a: Boolean) = {
  var b = true
  a && { b = false; true }
  b
} ensuring { res => res != a }

如果我在Scala控制台中测试这段代码，它就会像预期的那样工作。但是leon --xlang说后置条件是无效的。这是预期/指定的吗？

Answer 1

查看xlang转换阶段之后的(简化)编码，我们得到以下内容：

  def negate0(a0 : Boolean): Boolean = {
    val b1 = true
    val b2 = false
    b2
  } ensuring {
    res19 => res19 != a0
  }

第一个b1对应于初始化var b = true。引入第二个b2与赋值b = false相对应。不幸的是，XLang没有对&&和||操作符做任何特殊处理，这意味着它将提取子表达式中的所有副作用，并将它们移动到“顶层”级别(这就是为什么您有val b2 = false)。最后返回的值是b2 ( b的最后一个已知名称)，显然忽略了表达式a && ... (副作用除外)。

基本上，这是里昂的一个限制，我们将研究修复它。

编辑:注意，这个问题在里昂：https://github.com/epfl-lara/leon/commit/2485477f4e91cba7fe6e0c137817d62f513a3c42的最新版本中得到了修正。