Traits and class invariants

Jan 14, 2015 at 7:54 PM
I have a question about how to declare class invariants in traits.

I'd like to have trait T declare a method M. When class C extends trait T, class C must implement method M. C's implementation of M needs to know some invariant about C's state, so I declare a predicate Valid that must be satisfied before calling M:

trait T
{
predicate Valid() reads this;

method M()
    requires Valid();
    ensures  Valid();
}

class C extends T
{
var x:int;

predicate Valid() reads this; { x >= 0 }

constructor C() modifies this; ensures Valid(); { x := 5; }

method M()
    requires Valid();
    ensures  Valid();
{
    assert x >= 0;
}
}

However, C's declaration of M produces the following error:
Error: the method must provide an equal or more permissive precondition than in its parent trait
Is this an expected error? Is there a way to enforce class invariants in methods when using traits?