Skip to content

Add Max and Min functions with properties tests #172

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
leozou2004 wants to merge 9 commits into
base: main
Choose a base branch
from
Open

Add Max and Min functions with properties tests #172

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
aff4dbb
Add Max and Min functions with properties tests
leozou2004 Dec 1, 2025
e0320cf
Updated test case
leozou2004 Dec 2, 2025
2590d34
Added proof for min max properties
leozou2004 Dec 2, 2025
d78da5c
Rename MaxMin.dfy to max_min_properties.dfy for consistency
leozou2004 Dec 2, 2025
4abb827
Apply suggestions from code review
myf07 Dec 2, 2025
f078da5
Merge branch 'utgheith:main' into add-max-properties-test
leozou2004 Dec 2, 2025
0673078
Merge branch 'utgheith:main' into add-max-properties-test
leozou2004 Dec 3, 2025
5ef9ef8
Added a bit of complexity so the proof doesn't directly pass
leozou2004 Dec 3, 2025
c8ef9c7
change proof file to correspond with the test file
leozou2004 Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 24 additions & 0 deletions proofs/max_min_properties.dfy
View file
Open in desktop
Copy link
Collaborator

@myf07 myf07 Dec 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Author

@leozou2004 leozou2004 Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok I think i have fixed this now.

Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
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 a <= b ==> Max(a, b) == b && Min(a, b) == a
ensures b <= a ==> Max(a, b) == a && Min(a, b) == b
{
}

59 changes: 59 additions & 0 deletions testcases/max_min_properties.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
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
}

// Test 1: bounds + “returns one of the arguments”.
method {:induction false} Test_MaxMin_Bounds(a: int, b: int)
{
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);
}
}

// 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);
}
}

// Test 3: case-wise behavior (ordering).
method {:induction false} Test_MaxMin_Relation(a: int, b: int)
{
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);
}
}
}