unclear behaviour of traits and test type in Dafny

Question

I am trying to understand how Dafny handles postconditions of concrete classes. In the example below, I have two classes B and C that extend a trait A. Both have different postconditions for the method m.

The methods test and test2 take in input an object el of type A and call the method m -- I would like them to verify, but I don't know if there is an easy way to do that.

Finally, in the method test3, I take an element from a set of objects of type A. If I later test the type of the element to be of type C, then Dafny produce the error `cannot establish the existence of LHS values that satisfy the such-that predicate' and seems to assume everywhere that the element is of type C.

trait A {
    var a: int
    method m()
        modifies this
}

class B extends A {
    method m()
        modifies this
        ensures this.a > 5 
    {
        a := 10;
    }
}

class C extends A {
    method m() 
        modifies this
        ensures this.a < -5
    {
        a := -10;
    }
}


method test(el : A)
    modifies el
{
    el.m();
    if (el is C)
    {
        assert el.a < -5;
    }
    if (el is B)
    {
        assert el.a > 5;
    }
    
}

method test2(el : A)
    modifies el
{
    
    if (el is C)
    {
        assert (el is C);
        el.m();
        assert el.a < -5;
    }
    
    if (el is B)
    {
        el.m();
        assert el.a > 5;
    }
}


method test3(s : set<A>)
    modifies s
    requires s != {}
{
    var el :| el in s;
    if (el is C)
    {
        assert (el is C);
        el.m();
        assert el.a < -5;
    }
    
    if (el is B)
    {
        el.m();
        assert el.a > 5;
    }
}

Is it possible to make methods test and test2 verify, and what is the problem in test3? Thanks

Answer 1

I don't think you can make test work. For the other two cases, you may want to go with this:

trait A {
    var a: int
    method m()
        modifies this
}

class B extends A {
    method m()
        modifies this
        ensures this.a > 5 
    {
        a := 10;
    }
}

class C extends A {
    method m() 
        modifies this
        ensures this.a < -5
    {
        a := -10;
    }
}

method test2(el : A)
    modifies el
{
    
    if (el is C)
    {
        assert (el is C);
        var el: C := el;
        el.m();
        assert el.a < -5;
    }
    
    if (el is B)
    {
        var el: B := el;
        el.m();
        assert el.a > 5;
    }
}


method test3(s : set<A>)
    modifies s
    requires s != {}
{
    var el: A :| el in s;
    if (el is C)
    {
        assert (el is C);
        var el: C := el;
        el.m();
        assert el.a < -5;
    } 

    if (el is B)
    {
        var el: B := el;
        el.m();
        assert el.a > 5;
    }
}