Generic traits

Feb 13, 2016 at 12:59 PM
Hello,

I'm trying to define some abstract data types in Dafny and I have found generic traits interesting for that purpose. As I have read in Automatic Verification of Dafny Programs with Traits [krml247], it was a feature you were intended to add soon but it is not available nowadays (Error: sorry, traits with type parameters are not supported).

Will generic traits be available soon? Are there any suitable alternatives?

The intention is approximately:
trait Queue<T> {
    ghost var Elements : seq<T>;

    method Pop() returns (x : T)
        requires |Elements| > 0
        ensures Elements == old(Elements)[1..]
        ensures x == old(Elements)[0]

    method Push(x : T)
        ensures Elements == [x] + old(Elements)
}

class LinkedQueue<T> extends Queue<T> {
    // [...]
}

class ArrayQueue<T> extends Queue<T> {
    // [...]
}
Coordinator
Mar 5, 2016 at 6:02 PM
Thanks for your interest in traits. At the moment, there is no specific plan to extend the existing support of traits, since we have a number of development/support tasks of higher priority. However, your interest is duly noted. Feel free to file an "Issue", where we can track the to-do item. (Alternatively, if you are interested in going into the Dafny source to add this feature, I can provide a bit of handholding.)

Rustan