Dafny 中的多态性

Question

我正在尝试在 Dafny 中进行多态性，但我无法使其工作。我没有找到任何文档来帮助我解决这个问题。这是代码：https://rise4fun.com/Dafny/uQ1w

trait Atom {
  var Leaf? : bool;
}

class Leaf extends Atom {
  constructor() {
    this.Leaf? := true;
  }
}

class Node extends Atom {
  var left : Atom;

  constructor() {
    this.Leaf? := false;
    this.left := new Leaf();
  }
}

method Main() {
  var root := new Node();
  root.left := new Node();

  root.left.left := new Node();
}

错误：

Dafny 2.1.1.10209
stdin.dfy(24,12): Error: member left does not exist in trait Atom
1 resolution/type errors detected in stdin.dfy

Answer 1

表达式root.left 的类型为Atom（因为这是Node 类中left 字段的类型）。因此，类型系统不知道root.left指向的对象是Leaf还是Node，尤其不能保证这个对象有left属性。

您可以通过先将左孩子分配给变量，然后访问其next 属性来规避此问题：

method Main() {
  var root := new Node();

  // root_l is inferred to have type 'Node' instead of 'Atom'  
  var root_l := new Node();
  root.left := root_l;

  // Here root_l has type Node, so it has a 'left' attribute.
  root_l.left := new Node();
}

在面向对象的语言（例如 Java）中，这也可以通过向下转换来解决（例如 ((Node)root.left).left := new Node();，但我不知道 Dafny 是否支持这种转换。

Answer 2

对于这个特定的例子，使用datatype 是有意义的：

datatype Atom = Leaf | Node(left: Atom)

method Main() {
  var root := Atom.Node(Atom.Node(Atom.Leaf));
}

编译器为Atom 两种类型提供谓词atom.Leaf? 和atom.Node?。例如，root.Node? 是 true。