Dafny 中的多态性 [英] Polymorphism in Dafny

问题描述

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

I am trying to do polymorphism in Dafny but I can't make it work. I didn't find any documentation to help me with this. Here is the code: 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 指向的对象是 Leaf 还是 Node，特别是它无法确保此对象具有 left 属性.

The expression root.left has type Atom (since that is the type of left field in Node class). Therefore, the type system doesn't know whether the object pointed by root.left is a Leaf or a Node and, in particular, it cannot ensure that this object has a left attribute.

您可以通过先将左孩子分配给一个变量，然后访问它的 next 属性来规避这一点:

You can circumvent this by assigning the left child to a variable first, and then accessing its next attribute:

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 是否支持这种类型转换.

In an object-oriented language (e.g. Java), this can also be solved with the help of downcastings (for instance ((Node)root.left).left := new Node();, but I don't know whether such castings are supported in Dafny.

这篇关于Dafny 中的多态性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！