Dafny- 使用方法更改谓词的内部

Question

我在 Dafny 中写了一个 class，其形式为

class Question{

    var a: int;
    var b: seq<int>;

    predicate isValid(something: Type) { .... }

    method X(something : Type) returns (b : int)
   {
       //utilises b to calculate a value for a 
       .....
   }

   predicate Second(something: Type) { a == X(something) }

   //"something" is the same for all predicates and functions
}

我知道我不能调用 Second() 谓词中的方法，但我想断言整数 "a" 应该等同于给定变量 "something" 时的某个整数，使用 class 中定义的方法计算。有什么办法吗？

提前致谢。

Answer 1

正如我在评论中提到的，方法没有直接的方式来影响任何逻辑实体（例如谓词）。相反，你需要在一个函数中描述你关心的东西，然后你可以用它来谈论价值。

让我用您在评论中提到的示例代码来说明。考虑 Graph class 中的方法 w。此方法没有副作用，其 return 值将在进一步规范中有用。我们可以用函数 Weight 代替它，如下所示。

function Weight(u: int, v: int): int
reads this, this.edges, this.vertices
requires this.isValid() && this.hasEdge(u,v)
requires u < d.Length && v< d.Length
{
  var f : Edge? :| f in edges && f !=null && f.source == u && f.dest == v;
  f.weight
}

在这种情况下，它相对简单：主体基本上相同。

这是另一个更复杂的例子。考虑 Path class 中的 getL 方法。同样，这个方法是 side-effect 免费的，所以让我们用一个函数替换它。

function Length(G: Graph?): int
reads ...
requires ...
{
    Sum(0, |pv| - 1, i /* ... */ => G.Weight(pv[i].id, pv[i+1].id))
}

我们使用 G.Weight 和一个函数 Sum，其类型（大致）如下所示

function Sum(lo: int, hi: int, f: int -> int): int
decreases hi - lo
{
  if lo >= hi then 0
  else f(lo) + Sum(lo + 1, hi, f)
}

它在 [lo, hi) 范围内对 f 的值求和。

实际上，我们需要一个更强大的 Sum 版本，它允许 f 有一个前提条件，也可以读取堆。这是它的类型（相同的机身工作）。

function Sum(lo: int, hi: int, f: int ~> int): int
requires forall i | lo <= i < hi :: f.requires(i)
decreases hi - lo
reads set i, o | lo <= i < hi && o in f.reads(i) :: o

注意 -> 变成了 ~>，并且我们添加了 requires 和 reads 子句。

返回 Length，我们还需要填写一些缺失的 reads 和 requires 注释。这是完整的定义。

function Length(G: Graph): int
reads G, G.vertices, G.d , G.edges
reads this, this.pv
requires G != null && G.isValid() && this.isValid(G)
{
    Sum(0, |pv| - 1, i reads this, this.pv, G, G.edges, G.vertices, G.d
                       requires 0 <= i < |pv| - 1 && G.isValid() && this.isValid(G) =>
                       G.Weight(pv[i].id, pv[i+1].id))
}

这计算的值与 getL 相同，可用于规范。

希望对您有所帮助！

Dafny- 使用方法更改谓词的内部

Dafny- Using a method to change a inside of a predicate

oop

formal-verification

dafny