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);

但是我收到错误消息：

“ in”的第二个参数必须是集合，多集或序列类型为Alg的元素，或具有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)

[关于示例的另一条评论：您正在此处定义数学。当您这样做时，通常最好不要使用诸如类，方法和可变字段之类的命令性功能。您不需要这些功能，它们只会使数学复杂化。相反，我建议删除该类，将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)

Rustan