old expression in (ghost) predicates

Question

I am working on a Dafny project, where large (lots of characters) two-state post-conditions occurs. Such post-conditions may be repeated across different methods of a same class. I would like to define them in predicates, to get a better organized code. However, old expressions are not allowed in such contexts (same with `unchanged'). Does everyone has a workaround?

This is a small example

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

There is another keyword, twostate, that allows you to create predicates on frames.

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