Add Tower of Hanoi + Simple Arithmetic Tests#182
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds two new test cases with proof stubs for Dafny verification: a bubble sort implementation and a sum formula proof. The bubble sort includes helper lemmas to establish correctness properties such as length preservation, multiset preservation, and sorted order guarantees.
- Adds bubble sort test case with functions for single-pass and multi-pass sorting
- Adds sum formula test case comparing recursive and closed-form implementations
- Includes comprehensive proof stubs with helper lemmas for establishing sorting properties
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| testcases/sum_formula.dfy | Defines recursive sum function, closed-form formula, and test lemma |
| testcases/bubble_sort.dfy | Implements bubble sort with BubblePass and Sort functions, includes test method |
| proofs/sum_formula.dfy | Provides proof stub for sum formula equivalence |
| proofs/bubble_sort.dfy | Defines main correctness lemma and helper lemmas for sorting properties |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 4 out of 4 changed files in this pull request and generated 5 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| @@ -0,0 +1,5 @@ | |||
| lemma {:induction false} proof(n: nat) | |||
There was a problem hiding this comment.
The lemma name proof is too generic and doesn't follow the naming convention used by most other test cases in this repository. Consider using a more descriptive PascalCase name like SumEqualsFormulaProof to match the pattern used in other files (e.g., AddAllProof, ExpPositiveProof, PrimeDivisorLemma).
| lemma {:induction false} proof(n: nat) | |
| lemma {:induction false} SumEqualsFormulaProof(n: nat) |
| lemma {:induction false} sorting_correctness(s: seq<int>) | ||
| ensures |Sort(s)| == |s| && | ||
| forall i: int, j: int :: 0 <= i < j < |Sort(s)| ==> Sort(s)[i] <= Sort(s)[j] | ||
| decreases |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} bubble_pass_preserves_length(s: seq<int>) | ||
| ensures |BubblePass(s)| == |s| | ||
| decreases |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} sort_helper_preserves_length(s: seq<int>, n: int) | ||
| requires 0 <= n | ||
| ensures |SortHelper(s, n)| == |s| | ||
| decreases n | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} bubble_pass_preserves_multiset(s: seq<int>) | ||
| ensures (forall x :: x in multiset(s) ==> x in multiset(BubblePass(s))) && | ||
| (forall x :: x in multiset(BubblePass(s)) ==> x in multiset(s)) | ||
| decreases |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} bubble_pass_elements_from_original(s: seq<int>, i: int) | ||
| requires 0 <= i < |BubblePass(s)| | ||
| ensures BubblePass(s)[i] in multiset(s) | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} element_in_multiset_bounded_by_max(s: seq<int>, elem: int) | ||
| requires elem in multiset(s) | ||
| requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1] | ||
| ensures elem <= s[|s| - 1] | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} bubble_pass_moves_max_to_end(s: seq<int>) | ||
| requires |s| > 0 | ||
| ensures forall i :: 0 <= i < |BubblePass(s)| - 1 ==> BubblePass(s)[i] <= BubblePass(s)[|BubblePass(s)| - 1] | ||
| decreases |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} bubble_pass_preserves_max_at_end(s: seq<int>) | ||
| requires |s| > 0 | ||
| requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1] | ||
| ensures BubblePass(s)[|BubblePass(s)| - 1] == s[|s| - 1] | ||
| decreases |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} bubble_pass_prefix_when_max_at_end(s: seq<int>) | ||
| requires |s| > 1 | ||
| requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1] | ||
| ensures BubblePass(s)[..|BubblePass(s)|-1] == BubblePass(s[..|s|-1]) | ||
| decreases |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} sort_helper_produces_sorted_sequence(s: seq<int>, n: int) | ||
| requires 0 <= n | ||
| requires n >= |s| | ||
| ensures forall i: int, j: int :: 0 <= i < j < |SortHelper(s, n)| ==> SortHelper(s, n)[i] <= SortHelper(s, n)[j] | ||
| decreases n, |s| | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} sort_helper_decomposes_with_max(s: seq<int>, n: int) | ||
| requires 0 <= n | ||
| requires |s| > 0 | ||
| requires forall i :: 0 <= i < |s| - 1 ==> s[i] <= s[|s| - 1] | ||
| ensures SortHelper(s, n) == SortHelper(s[..|s|-1], n) + [s[|s| - 1]] | ||
| decreases n | ||
| { | ||
|
|
||
| } | ||
|
|
||
| lemma {:induction false} sort_helper_preserves_upper_bound(s: seq<int>, n: int, bound: int) | ||
| requires 0 <= n | ||
| requires forall i :: 0 <= i < |s| ==> s[i] <= bound | ||
| ensures forall i :: 0 <= i < |SortHelper(s, n)| ==> SortHelper(s, n)[i] <= bound | ||
| decreases n | ||
| { | ||
|
|
||
| } | ||
|
|
There was a problem hiding this comment.
The lemma names in this file use snake_case (e.g., sorting_correctness, bubble_pass_preserves_length), which is inconsistent with the PascalCase naming convention used for lemmas throughout the rest of the repository (e.g., AddAllProof, ExpPositiveProof, PrimeDivisorLemma). Consider renaming to use PascalCase for consistency.
| ghost function {:induction false} SortHelper(s: seq<int>, n: int): seq<int> | ||
| decreases n | ||
| { | ||
| if n <= 0 then s // sorted |
There was a problem hiding this comment.
The comment // sorted is misleading. When n <= 0, the function simply returns the sequence s unchanged, which is not necessarily sorted. A more accurate comment would be // base case: no more passes or // assume sorted after |s| passes.
| if n <= 0 then s // sorted | |
| if n <= 0 then s // base case: no more passes |
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
The code looks good overall. The sum test is a good basic example, and the bubble sort test seems to make sense as well, but I have not tried working through filling out the stubs. Just to make copilot happy, maybe use Pascal case. The content itself looks good. |
|
Bubble sort is already a private TC, and as such, I do not believe it would be a valid public TC. |
I agree on this. I'm not sure on the exact intended distinction but these better scoped for a private case. |
|
Shoot thanks for letting me know, I did not realize it was already a private TC |
Sarthak-Dayal
changed the title
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 4 out of 4 changed files in this pull request and generated 10 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Uh oh!
There was an error while loading. Please reload this page.