WIP: Enumerator<T> trait

examples/Enumerators/Datatypes.dfy

@@ -0,0 +1,87 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "Enumerators.dfy"
+
+// An example of an enumerator that traverses the sub-values in 
+// an algebraic datatype value.
+module DatatypeEnumerator {
+
+  import opened Enumerators
+
+  // TODO: A TreeEnumerator would be much more interesting!
+  // Show how to implement multiple traversal options, probably
+  // using ConcatEnumerator for child paths.
+
+  // TODO: Could define a Enumerable<T> trait as well, although datatypes
+  // can't yet implement that anyway.
+  datatype List<T> = Cons(value: T, tail: List<T>) | Nil {
+    method Enumerator() returns (e: Enumerator<T>) {
+      e := new ListEnumerator(this);
+    }
+
+    function Length(): nat {
+      match this
+      case Cons(_, tail) => 1 + tail.Length()
+      case Nil => 0
+    }
+  }
+
+  class ListEnumerator<T> extends Enumerator<T> {
+
+    var next: List<T>
+
+    constructor(next: List<T>) 
+      ensures Valid()
+      ensures fresh(Repr - {this})
+    {
+      this.next := next;
+
+      enumerated := [];
+      Repr := {this};
+    }
+
+    predicate Valid() 
+      reads this, Repr 
+      ensures Valid() ==> this in Repr 
+      decreases Repr, 0
+    {
+      && this in Repr
+    }
+
+    function Decreases(): nat
+      reads Repr
+      requires Valid()
+      decreases Repr, 1
+    {
+      // TODO: This is where I wish I could just say "next" and 
+      // rely on the well-founded ordering.
+      next.Length()
+    }
+
+    predicate method HasNext() 
+      reads Repr
+      requires Valid()
+      decreases Repr, 2
+      ensures Decreases() == 0 ==> !HasNext()
+    {
+      next.Cons?
+    }
+
+    method Next() returns (element: T)
+      requires Valid()
+      requires HasNext()
+      modifies Repr
+      decreases Repr
+      ensures Valid()
+      ensures Repr <= old(Repr)
+      ensures Decreases() < old(Decreases())
+      ensures enumerated == old(enumerated) + [element]
+    {
+      element := next.value;
+      next := next.tail;
+
+      enumerated := enumerated + [element];
+    }
+  }
+}

examples/Enumerators/Datatypes.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 12 verified, 0 errors

examples/Enumerators/Enumerators.dfy

@@ -0,0 +1,143 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "../../src/Enumerators/Enumerators.dfy"
+
+module Demo {
+
+  import opened Enumerators
+
+  // Note the common template for using a while loop on
+  // an arbitrary Enumerator. This will likely be what we
+  // propose that a "foreach" loop in Dafny will desugar to.
+
+  method Example1() {
+    var numbers := [1, 2, 3, 4, 5];
+
+    var e: Enumerator<int> := new SeqEnumerator(numbers);
+    while (e.HasNext()) 
+      invariant e.Valid() && fresh(e.Repr)
+      decreases e.Decreases()
+    {
+      var element := e.Next();
+
+      print element, "\n";
+    }
+  }
+
+  method Example2() {
+    var first := [1, 2, 3, 4, 5];
+    var second := [6, 7, 8];
+    var e1 := new SeqEnumerator(first);
+    var e2 := new SeqEnumerator(second);
+    var e := new ConcatEnumerator(e1, e2);
+
+    while (e.HasNext()) 
+      invariant e.Valid() && fresh(e.Repr)
+      decreases e.Decreases()
+    {
+      var element := e.Next();
+
+      print element, "\n";
+    }
+  }
+
+  method PrintWithCommas() {
+    var first := [1, 2, 3, 4, 5];
+    var e := new SeqEnumerator(first);
+
+    while (e.HasNext()) 
+      invariant e.Valid() && fresh(e.Repr)
+      decreases e.Decreases()
+    {
+      var element := e.Next();
+
+      print element;
+      if e.HasNext() {
+        print ", ";
+      }
+    }
+    print "\n";
+  }
+
+  method MappingExample() {
+    var first := [1, 2, 3, 4, 5];
+    var e1 := new SeqEnumerator(first);
+    var e := new MappingEnumerator(x => x + 2, e1);
+
+    var result: seq<int> := [];
+    while (e.HasNext()) 
+      invariant e.Valid() && fresh(e.Repr)
+      decreases e.Decreases()
+    {
+      var element := e.Next();
+
+      result := result + [element];
+    }
+    assert e.enumerated == Seq.Map(x => x + 2, first);
+  }
+
+  // Some examples showing the equivalence between enumerator
+  // operations and sequence operations.
+
+  method RoundTrip(s: seq<nat>) returns (result: seq<nat>)
+    ensures result == s
+  {
+    var e: Enumerator := new SeqEnumerator(s);
+    result := CollectToSeq(e);
+  }
+
+  method AddTwoToEach(s: seq<nat>) returns (result: seq<nat>)
+    ensures result == Seq.Map(x => x + 2, s)
+  {
+    var e := new SeqEnumerator(s);
+    var mapped := new MappingEnumerator(x => x + 2, e);
+    result := CollectToSeq(mapped);
+  }
+
+  method SetToSeq<T>(s: set<T>) returns (result: seq<T>)
+    ensures multiset(result) == multiset(s)
+  {
+    var e := new SetEnumerator(s);
+    result := CollectToSeq(e);
+  }
+
+  method Filter<T>(s: seq<T>, p: T -> bool) returns (result: seq<T>)
+    ensures result == Seq.Filter(p, s)
+  {
+    var e := new SeqEnumerator(s);
+    var filtered: FilteredEnumerator := new FilteredEnumerator(e, p);
+    result := CollectToSeq(filtered);
+    assert filtered.Valid();
+  }
+
+  method Concatenate<T>(first: seq<T>, second: seq<T>) returns (result: seq<T>)
+    ensures result == first + second
+  {
+    var e1 := new SeqEnumerator(first);
+    var e2 := new SeqEnumerator(second);
+    var concatenated: ConcatEnumerator := new ConcatEnumerator(e1, e2);
+    result := CollectToSeq(concatenated);
+    assert concatenated.Valid();
+  }
+
+  // TODO: The examples above work because Dafny is aware of the concrete
+  // types of the various enumerator values, and hence knows the additional post-conditions
+  // of Valid() and !HasNext() necessary to support the more specific assertions.
+  // That's why we need to explicitly attach a more specific type than Enumerator
+  // to some variables, when type inference would otherwise choose Enumerator.
+  // This will be an issue when trying to add more higher-order operations on enumerators,
+  // or on linking to external implementations that don't have specific Dafny types to
+  // attach their invariants on. 
+  //
+  // We'd like to have signatures like this, that ensures the Valid() and HasNext() 
+  // implementations on the result have the desired properties, so we don't need the 
+  // verifier to know the concrete type of the result:
+  //
+  // method MakeSeqEnumerator<T>(s: seq<T>) returns (result: Enumerator<T>)
+  //   ensures forall e :: (result's HasNext applied to e) == false ==> e.enumerated == s)
+  //
+  // There isn't currently any way to refer to the HasNext function on the result that doesn't
+  // bind result as the function receiver, though, and my attempts to define ghost vars that
+  // hold onto such function references haven't worked out well so far.
+}

examples/Enumerators/Enumerators.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 11 verified, 0 errors

examples/Enumerators/IteratorAdaptor.dfy

@@ -0,0 +1,104 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "../../src/Enumerators/Enumerators.dfy"
+include "../../src/Wrappers.dfy"
+
+// Dafny iterators do not share any common supertype, so there isn't
+// currently any way to write a single adaptor from an arbitrary
+// iterator to the Enumerator<T> trait. However, this example should
+// serve as a template for adapting any specific iterator.
+//
+// In practice, a loop that uses a specific iterator type will need to
+// declare a "decreases" termination metric, and hence the iterator
+// in question will need at least one "yield ensures" clause to
+// support such a metric. The same is true for adapting a specific iterator
+// to the Enumerator<T> trait in order to implement the Decreases() function.
+module IteratorAdaptorExample {
+
+  import opened Enumerators
+  import opened Wrappers
+
+  iterator RangeIterator(start: int, end: int) yields (element: int)
+    requires start <= end
+    // This is necessary in order to prove termination via Decreases()
+    yield ensures element - start + 1 == |elements|
+    // This is necessary to prove the Repr <= old(Repr) post-condition
+    // of Next(). Iterators that instantiate and "hand off" objects
+    // will need a weaker post-condition.
+    yield ensures _new == {};
+    ensures |elements| == end - start
+  {
+    for i := start to end
+      invariant i - start == |elements|
+      invariant _new == {}
+    {
+      yield i;
+    }
+  }
+
+  class RangeEnumerator extends Enumerator<int> {
+
+    const iter: RangeIterator
+    var remaining: nat
+
+    constructor(start: int, end: int) 
+      requires start <= end
+      ensures Valid() 
+      ensures fresh(Repr) 
+    { 
+      iter := new RangeIterator(start, end);
+      remaining := end - start;
+      enumerated := [];
+
+      new;
+
+      Repr := {this, iter};
+    }
+
+    predicate Valid()
+      reads this, Repr
+      ensures Valid() ==> this in Repr 
+      decreases Repr, 0
+    {
+      && this in Repr
+      && iter in Repr
+      && iter._modifies + iter._reads + iter._new == {}
+      && iter.Valid()
+      && remaining == (iter.end - iter.start) - |iter.elements|
+    } 
+
+    predicate method HasNext()
+      requires Valid()
+      reads this, Repr
+      decreases Repr, 2
+      ensures HasNext() ==> Decreases() > 0
+    {
+      remaining > 0
+    }
+
+    method Next() returns (element: int)
+      requires Valid()
+      requires HasNext()
+      modifies Repr
+      decreases Repr
+      ensures Valid()
+      ensures Repr <= old(Repr) 
+      ensures Decreases() < old(Decreases())
+      ensures enumerated == old(enumerated) + [element]
+    {
+      var more := iter.MoveNext();
+      element := iter.element;
+      enumerated := enumerated + [element];
+      remaining := remaining - 1;
+    }
+
+    function Decreases(): nat 
+      reads this, Repr 
+      requires Valid()
+      decreases Repr, 1
+    {
+      remaining
+    }
+  }
+}

examples/Enumerators/IteratorAdaptor.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 12 verified, 0 errors