Question regarding interfaces and classes

Jul 25, 2013 at 4:40 PM
Edited Jul 25, 2013 at 4:41 PM
Hello,

First Question:
Does Dafny support using interfaces with classes? For example, can a class implement an interface like the following (pseudo-Java) example: (some what 'classic' polymorphism pattern)
main() {
  Shape shape = new Circle();
  shape.draw();
}

interface Shape {
  void draw();
}

class Circle implements Shape {
   public Circle() { } 

   public void draw() {
       // implementation for drawing circle
    }
}
I did notice in the modules tutorial (http://rise4fun.com/Dafny/tutorial/Modules) that you can create a level of abstraction with modules (i.e. using modules with interfaces), but I wasn't certain that would solve my problem (see second question below).

Second question:
In Dafny, can methods accept a parameter which is an 'interface' type (such as Enqueue( item : Queueable )) ?

The reason I'm looking into using classes with interfaces is I'm working on a project which we are trying to verify a priority queue, FIFO queue, and an unordered list. These queues (and a list) have a formal spec written in Z (a 'Zed' model) we are porting to Dafny. We wanted the queue items to be any data type and not 'tied' to one implementation. We were looking to do something like this:
class PriorityQueue<T> {
  ..
   method enqueue ( item : Queueable )    // Queueable would be an 'interface' type
      // pre and post conditions
   {
       /* 
      Since its a priority queue and the items are sorted, the queueable item would allow   comparison of two items for sorting the items in the queue.  For example, we want
        item.CompareTo(item2) == 0  to check if queue items are the same or less than and greater than with the appropriate code, if needed.  
     */
   }
  ..
}
However, I did see something close to this with a different queue (SimpleQueue class) which is right from one of Rustan Leino's papers: http://rise4fun.com/Dafny/xkWr . If the SimpleQueue was modified into a priority queue, I don't see how d : Data in Enqueue(d : Data) could get sorted when inserted into the priority queue. This example does not seem to mimic an interface to the extent I'm looking for.

I'm willing to post the priority queue I've created, but its quite messy so far.

Any help, assistance, or direction is much appreciated.

Best,

Matt
Jul 30, 2013 at 4:42 PM
I found the answer is no, cannot do it. According to Benchmark 3, a generically typed queue could not get sorted. Based on this, I'm assuming a generically typed priority queue would also not be possible.

These benchmarks were a few years old (I think). So, is it still true Dafny cannot sort a generically typed queue?

Best,

Matt