WIP: Enumerator<T> trait #37
Conversation
src/Enumerators/Enumerators.dfy
Outdated
| reads Repr | ||
| requires Valid() | ||
| decreases Repr, 2 | ||
| ensures HasNext() ==> Decreases() > 0 |
There was a problem hiding this comment.
For an enumerator that correctly implements Next(), L58 will have to hold of HasNext(). However, I don't see that any client of HasNext() needs to know this, so I suggest dropping L58.
There was a problem hiding this comment.
You're right, this is redundant since it follows from the decreasing post-condition of Next() itself. We need that "extraneous specification" linter :)
src/Enumerators/Enumerators.dfy
Outdated
| // Next() is invoked. This avoids forcing the type parameter for any | ||
| // enumerator to satisfy the Auto-initializable type characteristic (0), |
There was a problem hiding this comment.
I don't see anything in this trait that would require T to be an auto-init type. There is such a requirement on the yields parameters of an iterator, but I don't see that that also has to apply here.
It is quite possible that "knowing ahead of time if [an enumerator] is able to produce a value" requires the enumerator's constructor and Next() method to have to go compute the next value. Once that is computed, it needs to be stored in some field (call it next), so that the subsequent Next() has the precomputed value to return. If the pre-computation determines that there is no next value, then next still has to have a value. This is where it may look like an auto-init type is helpful. However, this problem is better solved by declaring next to have type Option<T>, just as class FilteredEnumerator is doing below.
There was a problem hiding this comment.
Those are exactly the details I had in my head when writing that. I'll either expand this or not bother mentioning it at this point.
src/Enumerators/Enumerators.dfy
Outdated
| // Pre-condition for Next(). Making this a pure predicate means that | ||
| // enumerators have to at least know ahead of time if they are able to | ||
| // produce a value, even if they do not know what value it is until |
There was a problem hiding this comment.
I'm not convinced this is the best model for enumerators. Always having to compute a value ahead of requests makes the code more complicated. And it may also be confusing, because any side effects of computing a value take place when the previous value is in the process of being returned.
There was a problem hiding this comment.
Completely agree on those downsides. My strongest reason for landing on this version so far is that it was FAR easier to make all this code verify. Now that I've reached this baseline, though, I'll make an alternate version of all of this where Next() returns an Option<T> instead and see how it compares on both the implementation and consuming sides.
examples/Enumerators/Enumerators.dfy
Outdated
| // 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 |
There was a problem hiding this comment.
Where is this needed? For all new allocations in this Demo module, I gave the trait as an explicit type of the receiving variable and everything still verifies. For example, I changed the declarations of e1, e2, and e in Example2() to
var e1: Enumerator := new SeqEnumerator(first);
var e2: Enumerator := new SeqEnumerator(second);
var e: Enumerator := new ConcatEnumerator(e1, e2);There was a problem hiding this comment.
Example2 is just fine with that because it doesn't assert anything about the behavior of the enumerators. But Concatenate has a post-condition that isn't verified if I remove the explicit type declaration on L119. That's because it needs the extra post-condition implied by !ConcatEnumerator.HasNext(), so Dafny doesn't have enough information if I don't guide it to recognize the concrete type of that enumerator. I'm trying to figure out if there's a better solution there.
There was a problem hiding this comment.
Ah don't spend any further thought on this, I have a solution that seems to work nicely. Will push something tomorrow.
This reverts commit bad3054.
This is an early draft of a design for an
Enumerable<T>trait, which I developed in the process of writing up an RFC for adding some kind of enumeration support to Dafny: dafny-lang/dafny#1753I do NOT expect this to be approved even once it is more polished, since it has the same issue with needing the
{:termination false}attribute that my other PR (#22) is blocked by. I will likely tackle at least a partial solution to that issue (dafny-lang/dafny#1588) before promoting this PR out of draft. I nevertheless wanted to create this PR for early feedback and as evidence that all the common enumeration use cases therein do in fact verify, and therefore to support the arguments in the RFC I'll be posting todafny-lang/rfcsshortly.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.