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

Question

我在Dafny中定义了一个西格玛代数数据类型，如下所示：

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 的地图

我想声明这样的属性：">存在一个代数，这样…"，或">for all algebratics…

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