inheritance and invariants

Jul 15, 2010 at 9:42 AM

Hi, I am having trouble establishing invariants for inherited classes after a constructor.

For example here, basically, the inheriting class contains an extra int field that is passed the same value as the int field 'val' that it inherits from TreeNode.

It flags 'object invariant might not hold' after leaving the constructor. I've also tried making the call base(v) inside the constructor, as shown, and have dabbled with Delayed/NotDelayed to no avail.

I have used [Additive], additive expose etc, in the base class, and this is the only message that I am getting.

I kind of feel the object invariant should hold (as they equal the same value),  but am I going wrong somewhere here in my understanding of things? Thanks!

class CompNode : TreeNode
    [SpecPublic] int sum;
    invariant val<=sum;        //DOES NOT HOLD
    public CompNode(int v): base(v)
        requires 0<v;
        ensures sum <= v;
        left = null;
        right = null;

        parent = null;

        sum = v;
       // base(v);  //I've tried base(v) at different points inside constructor