From aff4dbb0a0819373a0ff951e59804b48741a7768 Mon Sep 17 00:00:00 2001 From: leozou2004 <66689225+leozou2004@users.noreply.github.com> Date: Mon, 1 Dec 2025 17:37:20 -0600 Subject: [PATCH 1/7] Add Max and Min functions with properties tests Tests the common properties of max and min functions --- testcases/max_min_properties.dfy | 38 ++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 testcases/max_min_properties.dfy diff --git a/testcases/max_min_properties.dfy b/testcases/max_min_properties.dfy new file mode 100644 index 0000000..fa8ea21 --- /dev/null +++ b/testcases/max_min_properties.dfy @@ -0,0 +1,38 @@ +function {:induction false} Max(a: int, b: int): int +{ + if a >= b then a else b +} + +function {:induction false} Min(a: int, b: int): int +{ + if a <= b then a else b +} + +method {:induction false} MaxMinPropertiesTest(a: int, b: int) +{ + // 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; +} From e0320cfd87128a5364c9f43b1ef0e423f268e71c Mon Sep 17 00:00:00 2001 From: leozou2004 <66689225+leozou2004@users.noreply.github.com> Date: Mon, 1 Dec 2025 19:05:22 -0600 Subject: [PATCH 2/7] Updated test case --- testcases/max_min_properties.dfy | 65 ++++++++++++++++++++------------ 1 file changed, 41 insertions(+), 24 deletions(-) diff --git a/testcases/max_min_properties.dfy b/testcases/max_min_properties.dfy index fa8ea21..60555f9 100644 --- a/testcases/max_min_properties.dfy +++ b/testcases/max_min_properties.dfy @@ -1,3 +1,6 @@ +// MaxMin.dfy +// Basic properties of Max and Min on integers. + function {:induction false} Max(a: int, b: int): int { if a >= b then a else b @@ -8,31 +11,45 @@ function {:induction false} Min(a: int, b: int): int if a <= b then a else b } -method {:induction false} MaxMinPropertiesTest(a: int, b: int) +// Test 1: bounds + “returns one of the arguments”. +method {:induction false} Test_MaxMin_Bounds(a: int, b: int) { - // 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; + assert + Max(a, b) >= a && + Max(a, b) >= b && + Min(a, b) <= a && + Min(a, b) <= b && + (Max(a, b) == a || Max(a, b) == b) && + (Min(a, b) == a || Min(a, b) == b) + by + { + MaxMin_Bounds(a, b); + } +} - // Relation between Max and Min - assert Min(a, b) <= Max(a, b); +// Test 2: commutativity + idempotence. +method {:induction false} Test_MaxMin_Symmetry(a: int, b: int) +{ + assert + Max(a, b) == Max(b, a) && + Min(a, b) == Min(b, a) && + Max(a, a) == a && + Min(a, a) == a + by + { + MaxMin_Symmetry(a, b); + } +} - // Sum identity - assert Max(a, b) + Min(a, b) == a + b; +// Test 3: ordering + sum identity. +method {:induction false} Test_MaxMin_Relation(a: int, b: int) +{ + assert + Min(a, b) <= Max(a, b) && + Max(a, b) + Min(a, b) == a + b + by + { + MaxMin_Relation(a, b); + } } + From 2590d3464d9717a49251ce8e4299e9762ed366fb Mon Sep 17 00:00:00 2001 From: leozou2004 <66689225+leozou2004@users.noreply.github.com> Date: Mon, 1 Dec 2025 19:06:06 -0600 Subject: [PATCH 3/7] Added proof for min max properties --- proofs/MaxMin.dfy | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 proofs/MaxMin.dfy diff --git a/proofs/MaxMin.dfy b/proofs/MaxMin.dfy new file mode 100644 index 0000000..fd06ec6 --- /dev/null +++ b/proofs/MaxMin.dfy @@ -0,0 +1,23 @@ +lemma {:induction false} MaxMin_Bounds(a: int, b: int) + ensures Max(a, b) >= a + ensures Max(a, b) >= b + ensures Min(a, b) <= a + ensures Min(a, b) <= b + ensures Max(a, b) == a || Max(a, b) == b + ensures Min(a, b) == a || Min(a, b) == b +{ +} + +lemma {:induction false} MaxMin_Symmetry(a: int, b: int) + ensures Max(a, b) == Max(b, a) + ensures Min(a, b) == Min(b, a) + ensures Max(a, a) == a + ensures Min(a, a) == a +{ +} + +lemma {:induction false} MaxMin_Relation(a: int, b: int) + ensures Min(a, b) <= Max(a, b) + ensures Max(a, b) + Min(a, b) == a + b +{ +} From d78da5c5ff8466631cd62166d32bff42c5d837f3 Mon Sep 17 00:00:00 2001 From: leozou2004 <66689225+leozou2004@users.noreply.github.com> Date: Mon, 1 Dec 2025 19:50:55 -0600 Subject: [PATCH 4/7] Rename MaxMin.dfy to max_min_properties.dfy for consistency --- proofs/{MaxMin.dfy => max_min_properties.dfy} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename proofs/{MaxMin.dfy => max_min_properties.dfy} (100%) diff --git a/proofs/MaxMin.dfy b/proofs/max_min_properties.dfy similarity index 100% rename from proofs/MaxMin.dfy rename to proofs/max_min_properties.dfy From 4abb827b2fd3024de073324d7fd4e9d128caed23 Mon Sep 17 00:00:00 2001 From: "Yifan (Michael) Ma" <113753631+myf07@users.noreply.github.com> Date: Mon, 1 Dec 2025 20:14:47 -0600 Subject: [PATCH 5/7] Apply suggestions from code review Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- testcases/max_min_properties.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/testcases/max_min_properties.dfy b/testcases/max_min_properties.dfy index 60555f9..f95b2e4 100644 --- a/testcases/max_min_properties.dfy +++ b/testcases/max_min_properties.dfy @@ -1,4 +1,4 @@ -// MaxMin.dfy +// max_min_properties.dfy // Basic properties of Max and Min on integers. function {:induction false} Max(a: int, b: int): int From 5ef9ef812a375e7ce44405e16f1d3f54394e7b4b Mon Sep 17 00:00:00 2001 From: leozou2004 <66689225+leozou2004@users.noreply.github.com> Date: Wed, 3 Dec 2025 16:45:16 -0600 Subject: [PATCH 6/7] Added a bit of complexity so the proof doesn't directly pass --- testcases/max_min_properties.dfy | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/testcases/max_min_properties.dfy b/testcases/max_min_properties.dfy index f95b2e4..2fd5309 100644 --- a/testcases/max_min_properties.dfy +++ b/testcases/max_min_properties.dfy @@ -1,6 +1,3 @@ -// max_min_properties.dfy -// Basic properties of Max and Min on integers. - function {:induction false} Max(a: int, b: int): int { if a >= b then a else b @@ -41,15 +38,22 @@ method {:induction false} Test_MaxMin_Symmetry(a: int, b: int) } } -// Test 3: ordering + sum identity. +// Test 3: case-wise behavior (ordering). method {:induction false} Test_MaxMin_Relation(a: int, b: int) { - assert - Min(a, b) <= Max(a, b) && - Max(a, b) + Min(a, b) == a + b - by - { - MaxMin_Relation(a, b); + if a <= b { + assert Max(a, b) == b && Min(a, b) == a + by + { + MaxMin_Relation(a, b); + } + } else { + assert Max(a, b) == a && Min(a, b) == b + by + { + MaxMin_Relation(a, b); + } } } + From c8ef9c7ed46a36ba9a4f013bc4f3ff5582d06207 Mon Sep 17 00:00:00 2001 From: leozou2004 <66689225+leozou2004@users.noreply.github.com> Date: Wed, 3 Dec 2025 16:46:00 -0600 Subject: [PATCH 7/7] change proof file to correspond with the test file --- proofs/max_min_properties.dfy | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/proofs/max_min_properties.dfy b/proofs/max_min_properties.dfy index fd06ec6..3da9c10 100644 --- a/proofs/max_min_properties.dfy +++ b/proofs/max_min_properties.dfy @@ -17,7 +17,8 @@ lemma {:induction false} MaxMin_Symmetry(a: int, b: int) } lemma {:induction false} MaxMin_Relation(a: int, b: int) - ensures Min(a, b) <= Max(a, b) - ensures Max(a, b) + Min(a, b) == a + b + ensures a <= b ==> Max(a, b) == b && Min(a, b) == a + ensures b <= a ==> Max(a, b) == a && Min(a, b) == b { } +