如何为可能为空的字段编写修改子句

Question

我正在尝试验证红黑树（最初是用Python编写的）。 RedBlackTree 类表示树中的节点，具有以下感兴趣的字段：

  var parent: RedBlackTree?
  var left: RedBlackTree?
  var right: RedBlackTree?

我正在研究一种向左旋转 RB 树的左旋转方法。该方法的原始 Python 代码如下所示：

    def RotateLeft(self) -> RedBlackTree:
        parent = self.parent
        right = self.right
        if right is None:
            return self
        self.right = right.left
        if self.right is not None:
            self.right.parent = self
        self.parent = right
        right.left = self
        if parent is not None:
            if parent.left == self:
                parent.left = right
            else:
                parent.right = right
        right.parent = parent
        return right

这是我迄今为止在 Dafny 中写的内容。

  method rotate_left() returns (result: RedBlackTree?)
    modifies this
    modifies this.parent
    modifies this.right
    // ???
  {
    var parent: RedBlackTree? := this.parent;
    var right: RedBlackTree? := this.right;
    if right == null {
      return this;
    }

    this.right := right.left;
    if this.right != null {
        this.right.parent := this; // error here
    }
    this.parent := right;
    right.left := this;

    if parent != null {
      if parent.left == this {
        parent.left := right;
      } else {
        parent.right := right;
      }
    }
    right.parent := parent;
    return right;
  }
}

问题出在

this.right.parent := this;

行。我不知道如何为该行编写修改子句。

像

modifies this.right.parent

这样的修改子句并不能修复有问题的行； Dafny 拒绝它并给出错误

target object might be null

，这是有道理的，因为

this.right

可以为空。像

modifies if this.right != null then this.right.parent else this.right

这样的子句也不起作用；感兴趣的线仍然有错误。
我应该写什么子句来修改可能为空字段

parent

的字段

this.right

？

Answer 1

使用类来验证规范的一般做法是创建一个有效谓词和一个代表与该对象包含/相关的所有对象的对象的幽灵代表集。

class RedBlackTree {
    var parent: RedBlackTree?
    var left: RedBlackTree?
    var right: RedBlackTree?
    var val: int
    ghost var repr: set<object>

    ghost predicate Valid() 
        reads this, repr
        decreases repr
    {
        this in repr &&
        (this.left != null ==>
        (this.left in repr
        && this !in this.left.repr
        && this.left.repr < repr
        && this.left.parent == this
        && this.left.Valid()
        ))
        && (this.right != null ==>
        (this.right in repr
        && this !in this.right.repr
        && this.right.repr < repr
        && this.right.parent == this
        && this.right.Valid())) &&
        (this.left != null && this.right != null ==> this.left.repr !! this.right.repr && this.repr == {this} + this.left.repr + this.right.repr)
        && (this.left != null && this.right == null ==> this.repr == {this} + this.left.repr)
        && (this.right != null && this.left == null ==> this.repr == {this} + this.right.repr)
        && (this.right == null && this.left == null ==> this.repr == {this})
    }

method rotate_left() returns (result: RedBlackTree?)
    requires this.Valid()
    modifies repr
    modifies this.parent
    modifies this.right
  {
    var parent: RedBlackTree? := this.parent;
    var right: RedBlackTree? := this.right;
    if right == null {
      return this;
    }

    this.right := right.left;
    if this.right != null {
        this.right.parent := this; // error here
    }
    this.parent := right;
    right.left := this;

    if parent != null {
      if parent.left == this {
        parent.left := right;
      } else {
        parent.right := right;
      }
    }
    right.parent := parent;
    return right;
  }
}