Conversation
There was a problem hiding this comment.
Pull request overview
This PR introduces comprehensive test cases for sequence compression algorithms in Dafny, specifically implementing and verifying Delta encoding and Run-Length Encoding (RLE) with formal proofs of their correctness properties.
Key changes:
- Implementation of Delta encoding/decoding and Run-Length Encoding/decoding functions
- Formal verification of round-trip properties for both compression methods
- Combined Delta+RLE pipeline with proof of correctness
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| testcases/delta_RLE.dfy | Defines compression functions (DeltaEncode/Decode, RunLengthEncode/Decode, ExpandRun) and a CompressionValidation method that tests round-trip properties |
| proofs/delta_RLE.dfy | Provides formal lemmas proving correctness of all compression algorithms, including DeltaRoundTrip, RLERoundTrip, and the combined DeltaRLERoundTrip properties |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| } else if |s| == 1 { | ||
| assert [(s[0], 1)] == RunLengthEncode(s); | ||
| assert RunLengthDecode([(s[0], 1)]) == ExpandRun((s[0], 1)); | ||
| assert ExpandRun((s[0], 1)) == [s[0]]; |
There was a problem hiding this comment.
Trailing whitespace at the end of this line.
| assert ExpandRun((s[0], 1)) == [s[0]]; | |
| assert ExpandRun((s[0], 1)) == [s[0]]; |
|
Looks great, the RLE is a really good testcase and nontrivial to prove. However, I believe the expectation for the testcase was that the proof be empty except for small stubs that serve as hints, not filled in, so people could come up with their own proofs. |
|
RLE Encode and Decode was already a private TC. Not sure what the status of dupes is ngl. |
|
I don't really think this should be a public test case as it's a bit complex and hard to follow. The primary purpose of public test cases should be to introduce people to Dafny. |
|
I also agree that this test case is too involved to be a public test case that is meant to introduce Dafny, I think the proofs are too hard for a beginner. |
|
If the proofs are already filled in I propose we leave this up and merge it, as an example rather than a testcase/challenge. Also, for those who had to Google these compression methods: |
|
I think I agree its a bit complex for a public TC. I did RLE because it seemed pretty simple, and then it wasn't. I also wasn't aware of the duplicate, so I apologize there. |
No description provided.