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 class 中 left 字段的类型）。因此，类型系统不知道 root.left 指向的 object 是 Leaf 还是 Node，特别是，它不能确保 [=31] =] 有一个 left 属性。

您可以通过先将左 child 分配给一个变量，然后访问其 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();
}

在object-oriented语言中（例如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.

Dafny 中的多态性

Polymorphism in Dafny

polymorphism

dafny