Add Max and Min functions with properties tests #172
Conversation
Tests the common properties of max and min functions
There was a problem hiding this comment.
Pull request overview
This PR introduces Max and Min utility functions in Dafny along with a comprehensive test method that verifies fundamental mathematical properties of these functions through formal assertions.
- Adds
MaxandMinfunctions that return the maximum and minimum of two integers respectively - Implements
MaxMinPropertiesTestmethod that formally verifies 7 key mathematical properties including commutativity, idempotence, bounds, and sum identity - Uses Dafny's formal verification capabilities to prove correctness properties at compile-time
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
I might be misunderstanding the project but I thought we were supposed to implement a feature with tests that needs a proof to verify, but with your existing testcase, it seems to verify without a proof file. Is this intentional or what should be proven in the proof file? |
|
I agree with @AmeyaPurao's comment. While I don't have the permission to reject this PR, I don't think this should be approved. For every test case, we prove our program (or some function/method) by a lemma that contains our proof. It seems like you are trying to fill in the proof via the properties you have in your method. I think rather you should have lemmas and proofs to prove your functions (in this case, Max/Min). So, please do setup a lemma for the students to fill in. Furthermore, it's the students' job to fill in the proof. So, please create a stub lemma where we can fill in the proof. |
testcases/max_min_properties.dfy
Outdated
| // Max is at least each argument | ||
| assert Max(a, b) >= a; | ||
| assert Max(a, b) >= b; | ||
|
|
||
| // Min is at most each argument | ||
| assert Min(a, b) <= a; | ||
| assert Min(a, b) <= b; | ||
|
|
||
| // Max and Min return one of the arguments | ||
| assert Max(a, b) == a || Max(a, b) == b; | ||
| assert Min(a, b) == a || Min(a, b) == b; | ||
|
|
||
| // Commutativity | ||
| assert Max(a, b) == Max(b, a); | ||
| assert Min(a, b) == Min(b, a); | ||
|
|
||
| // Idempotence | ||
| assert Max(a, a) == a; | ||
| assert Min(a, a) == a; | ||
|
|
||
| // Relation between Max and Min | ||
| assert Min(a, b) <= Max(a, b); | ||
|
|
||
| // Sum identity | ||
| assert Max(a, b) + Min(a, b) == a + b; |
There was a problem hiding this comment.
This (as indicated in my parent comment) seems to be the proof. For the public test cases, we don't want to be submitting proofs. Rather just submitting empty proofs (in the form of lemma stubs).
Please refer to some of the proofs/.... files in the repository for examples.
Hope this makes sense!
|
I agree with above comments. You can implement |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 2 out of 2 changed files in this pull request and generated 5 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
I believe I fixed it with my next two commits. Lmk if I need to change anything. |
|
I just tested with the implementation and proof outlines you provided and it seems to pass verification without filling anything out (might be simple enough for dafny to just figure it out). On a separate note, I think the proof file should be named the same as the test case. |
|
Thanks for bringing that up. I've changed the proof file name so they're the same now. |
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
There was a problem hiding this comment.
Right now, this proof stub directly passes and trivially proves the test case. I think the test case needs to include more things so that the proof would actually require code in the body of the function.
There was a problem hiding this comment.
Ok I think i have fixed this now.
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 2 out of 2 changed files in this pull request and generated no new comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
I believe the proof stub still passes without filling out the lemmas (although I could just be using the wrong version). It's also worth considering whether this adds new or interesting tests not already present in the public TCs. |
|
I experience the same thing as Ameya and myf07: the proof seems to pass as is, without modifying the |
5 participants
Tests the common properties of max and min functions