Dafny 中的多态性

debugcn 发表于 Dev

安德里奇·塞萨尔

我正在尝试在 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

曼努埃尔·黑山

表达式root.left具有类型Atom（因为这是类中left字段的Node类型）。因此，类型系统不知道所指向的对象root.left是 aLeaf还是 a 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 是否支持此类转换。

本文收集自互联网，转载请注明来源。

如有侵权，请联系[email protected] 删除。