2

我想验证以下代码

object Test {

    def test(a: Int): Int = {
      require(a > 0)

      var sum = 0
      var i = 0

      while(i < a) {
        sum = sum + i
        i = i + 1
      }

      return sum
    } ensuring(res => res=a(a-1)/2)
}

请帮助我如何使用 Leon 在线系统来验证上述代码

得到以下编译错误

10：可变变量（例如 'var x' 而不是 'val x'）需要 xlang 去糖

14：变异变量需要xlang去糖

9：可变变量（例如 'var x' 而不是 'val x'）需要 xlang 去糖

13：块表达式需要xlang去糖变异变量需要xlang去糖

12：块表达式需要xlang去糖而表达式需要xlang去糖

4

1 回答 1

2

您粘贴的代码还有其他一些问题，我认为这是复制/粘贴错误，因为您报告的错误不同，但这里是固定版本：

object Test {
  def test(a: Int): Int = ({
    require(a > 0)
    var sum = 0
    var i = 0
    while(i < a) {
      sum = sum + i
      i = i + 1
    }
    sum
  }) ensuring(res => res == a*(a-1)/2)  
}

值得注意的是，您在 Ensure 子句中使用了赋值，并且不应return与 with 一起使用，ensuring因为 Scala 只会快捷地确保并直接从函数返回。一般来说，不要return在 Leon 中使用，我还建议return在大多数情况下不要与 Scala 一起使用。你也有a(a-1)哪个不是用于乘法的有效 Scala 代码，你应该有a*(a-1).

现在，关于--xlangLeon 在线选项。您尝试验证的代码依赖于命令式编程（变量和循环），Leon 对命令式编程的支持来自一个名为xlang. 不幸的是，xlangLeon Online 的支持已停用，因为它在 Leon 的合成功能上表现不佳。我们正在努力改进该xlang模块，以便它可以与 Leon 的其他功能一起运行。希望这最终会发生。

同时，如果您希望使用上述命令式功能验证程序，您唯一的选择是从命令行运行 Leon，并带有以下--xlang选项：

./leon --xlang Test.scala

您可以在此处找到有关如何在系统上安装 Leon 的一些文档：https ://leon.epfl.ch/doc/installation.html

于 2016-03-14T15:16:24.680 回答