Add min heap public test case #189
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
There was a problem hiding this comment.
Pull request overview
This PR adds a comprehensive min heap implementation example in Dafny that demonstrates formal verification of a data structure against its specification. The implementation uses predicates to define the spec in terms of multisets, then proves that a binary tree-based implementation correctly satisfies this spec. The HeapInvariant is intentionally left as a stub for users to complete as an exercise.
- Defines a formal specification for min heap operations (Size, Insert, Top, Pop) using multiset-based predicates
- Implements these operations using a binary tree structure with formal proofs that each operation satisfies its specification
- Provides an exercise framework where users implement the HeapInvariant predicate
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| testcases/min_heap.dfy | Contains the min heap specification predicates and binary tree implementation with formal verification that each method satisfies its spec |
| proofs/min_heap.dfy | Provides a stub for the HeapInvariant predicate that students should implement as an exercise |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // --------- Min Heap Specification --------- | ||
|
|
||
| // Written as predicates that check the output instead of functions that produce the output | ||
| // because it's surprising hard to find the min of a multiset in a function :( |
There was a problem hiding this comment.
Spelling error: "surprising hard" should be "surprisingly hard".
Suggested change
| // because it's surprising hard to find the min of a multiset in a function :( | |
| // because it's surprisingly hard to find the min of a multiset in a function :( |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This test case first defines a min-heap spec in terms of multisets, with Size, Insert, Top, and Pop. It then defines an implementation of that spec using a binary tree data structure. Each method ensures that it matches the spec, thus making sure that the implementation is fully correct. The one missing piece of the whole thing is the Heap Invariant, which is left as an exercise in the proofs/min_heap.dfy file and shouldn't be too difficult.
Overall, while it's a lot of code, I think it's a good example of how to prove that an implementation fully satisfies a spec for a fairly basic data structure, and there's a fairly small part you actually have to fill in so it shouldn't be awful.