1

我编写了一个类，它表示集合 S 上的二元关系，具有两个字段：该集合 S 和从 S 中提取的第二组值对。该类定义了一系列关系属性，例如是单值的（即，是一个函数，在“isFunction()”谓词中定义）。在类定义之后，我尝试定义一些子集类型。一个旨在定义这些关系的子类型，这些关系实际上也是“函数”。它不工作，解码产生的错误代码有点困难。请注意，Valid() 和 isFunction() 谓词确实声明了“读取此内容；”。关于我应该在哪里寻找的任何想法？是不是 Dafny 看不出子集类型有人居住？有没有办法说服它是这样的？

    type func<T> = f: binRelOnS<T> | f.Valid() && f.isFunction()

[Dafny VSCode] 尝试见证 null：操作结果可能违反 'binRelOnS' 的子集类型约束

4

1 回答 1

1

子集类型和非空

表单的子集类型定义

type MySubset = x: BaseType | RHS(x)

MySubset作为一种类型引入，它代表满足布尔表达式x的类型值。由于 Dafny 中的每个类型都必须是非空的，因此有义务证明您声明的类型具有某些成员。Dafny 可能会找到一些候选值，并会尝试查看其中是否有任何一个满足。如果候选人不这样做，您会收到与您看到的一样的错误消息。有时，错误消息会告诉您 Dafny 尝试了哪些候选值。BaseTypeRHS(x)RHS

在您的情况下，Dafny 尝试的唯一候选值是 value null。正如詹姆斯指出的那样，该值null甚至没有达到一垒，因为BaseType在您的示例中是一种非空引用。如果您更改binRelOnS<T>为binRelOnS?<T>，则null有可能成为证明您的子集类型为非空的证人。

用户提供的证人

由于 Dafny 不太擅长提出候选证人，因此您可能必须自己提供一个。为此，您可以witness在声明的末尾添加一个子句。例如：

type OddInt = x: int | x % 2 == 1 witness 73

由于73满足 RHS 约束x % 2 == 1，Dafny 接受这种类型。在某些程序中，您心目中的见证可能仅在幽灵代码中可用。然后，您可以编写ghost witness而不是witness，这允许后续表达式是幽灵。幽灵见证可以用来让 Dafny 验证器相信一个类型是非空的，但它并不能帮助 Dafny 编译器初始化该类型的变量，因此您仍然需要自己初始化这些变量。

使用witness子句，您可以尝试使用您对子集类型的原始定义来提供您自己的见证func。但是，witness 子句采用表达式，而不是语句，这意味着您不能使用new. 如果您不关心编译程序并且愿意相信见证人的存在，您可以声明一个承诺返回合适见证人的无正文函数：

type MySubset = x: BaseType | RHS(x) ghost witness MySubsetWitness()

function MySubsetWitness(): BaseType
  ensures RHS(MySubsetWitness())

您将需要ghost witness或function method. 该函数MySubsetWitness将永远没有主体，因此您有可能在某些值满足方面犯错RHS。

该witness子句是在 Dafny 版本 2.0.0 中引入的。2.0.0 发行说明提到了这一点，但显然没有给出太多解释。如果您想查看更多示例，请在Dafny 测试套件witness中搜索该关键字。

类的子集类型

在您的示例中，如果您将基本类型更改为可能为空的引用类型：

type func<T> = f: binRelOnS?<T> | f.Valid() && f.isFunction()

那么您的下一个问题将是 RHS 取消引用f。您可以通过削弱子集类型约束来解决此问题，如下所示：

type func<T> = f: binRelOnS?<T> | f != null ==> f.Valid() && f.isFunction()

现在到了可能会破坏交易的部分。子集类型不能依赖于可变状态。这是因为类型是一个非常静态的概念（与规范不同，规范通常取决于状态）。如果一个值在某个时刻可以满足一个类型，然后在程序中的一些状态更改之后，不满足该类型，那将是一场灾难。（事实上​​，几乎所有具有子集/细化/依赖类型的类型系统都适用于函数式语言。）因此，如果您的ValidorisFunction谓词有一个reads子句，那么您就无法func按照您希望的方式进行定义。但是，只要两者Valid都只isFunction依赖const于类中字段的值，那么就不需要reads子句并且一切就绪。

鲁斯坦

于 2018-03-06T01:25:33.023 回答