在 Dafny 中表达归纳数据类型的属性

Question

我在Dafny中定义了一个sigma代数数据类型，如下图：

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)

class test {

    var S : set<int>

    function eval(X: Alg) : set<int>  // evaluates an algebra
        reads this;
        decreases X;
    {
        match X
        case Empty => {}
        case Complement(a) => S - eval(X.a)
        case Union(b,c) => eval(X.b) + eval(X.c)
        case Set(s) => X.s
    }
}

我想说明量化归纳数据类型的属性。是否可以这样表达属性？

这是我尝试过的示例：

lemma algebra()
    ensures exists x :: x in Alg ==> eval(x) == {};
    ensures forall x :: x in Alg ==> eval(x) <= S;
    ensures forall x :: x in Alg ==> exists y :: y in Alg && eval(y) == S - eval(x);
    ensures forall b,c :: b in Alg && c in Alg ==> exists d :: d in Alg && eval(d) == eval(b) + eval(c);

但我收到错误消息：

second argument to "in" must be a set, multiset, or sequence with elements of type Alg, or a map with domain Alg

我想声明如下属性：“存在这样的代数...”，或“对于所有代数...".

Answer 1

类型与 Dafny 中的集合不同。你想在你的引理中表达量词如下：

lemma algebra()
  ensures exists x: Alg :: eval(x) == {}
  ensures forall x: Alg :: eval(x) <= S
  ensures forall x: Alg :: exists y: Alg :: eval(y) == S - eval(x)
  ensures forall b: Alg, c: Alg :: exists d: Alg :: eval(d) == eval(b) + eval(c)

同理，你可以声明一个变量x的类型为int，但你不要写成x in int.

由于类型推断，您不必显式地编写 : Alg。你可以只写：

lemma algebra()
  ensures exists x :: eval(x) == {}
  ensures forall x :: eval(x) <= S
  ensures forall x :: exists y :: eval(y) == S - eval(x)
  ensures forall b, c :: exists d :: eval(d) == eval(b) + eval(c)

对该示例的另一条评论：您在这里定义数学。当您这样做时，远离命令式功能（例如 classes、方法和可变字段）通常是个好主意。您不需要这些功能，它们只会使数学复杂化。相反，我建议删除 class，将 S 的声明更改为 const，并删除 reads 子句。那给你：

datatype Alg = Empty | Complement(a: Alg) | Union(b: Alg, c: Alg) | Set(s: set<int>)

const S: set<int>

function eval(X: Alg): set<int>  // evaluates an algebra
  decreases X
{
  match X
  case Empty => {}
  case Complement(a) => S - eval(X.a)
  case Union(b,c) => eval(X.b) + eval(X.c)
  case Set(s) => X.s
}

lemma algebra()
  ensures exists x :: eval(x) == {}
  ensures forall x :: eval(x) <= S
  ensures forall x :: exists y :: eval(y) == S - eval(x)
  ensures forall b, c :: exists d :: eval(d) == eval(b) + eval(c)

鲁斯坦

在 Dafny 中表达归纳数据类型的属性

expressing properties of inductive datatypes in Dafny

properties

algebraic-data-types

quantifiers

dafny