（幽灵）谓词中的旧表达式

Question

我正在开发一个 Dafny 项目，其中会发生大量（大量字符）两种状态后置条件。这样的后置条件可以在同一类的不同方法中重复。我想在谓词中定义它们，以获得更好组织的代码。然而，在这种情况下不允许使用旧的表达式（与“unchanged”相同）。 大家都有办法解决吗？

这是一个小例子

class A {
    
    var v : int
    // this is ok
    method M ()
        modifies this
        ensures v == old(v)
    
    // this is an hack that I don't want to use
    ghost predicate post(a : int, b : int)
        reads this
    {
        a == b
    }
    
    method M1 ()
        modifies this
        ensures post(v, old(v))

    
    // this is what i would like
    ghost predicate post()
        reads this
    {
        v == old(v)
    }
    
    method M2 ()
        modifies this
        ensures post()

}

Answer 1

还有另一个关键字，

twostate

，它允许您在框架上创建谓词。

    twostate predicate post()
        reads this
    {
        v == old(v)
    }