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()
}
There is another keyword, twostate
, that allows you to create predicates on frames.
twostate predicate post()
reads this
{
v == old(v)
}