Proving that this code is finding if the year is a leap year

Question

I have to write a code that tells me if a specific year of the gregorian calendar is leap year. However I'm not sure that the code will work for every every year. It works for 1900, 1901, 2000.

Before I paste the code, maybe you should know what make a gregorian year a leap year: If the year modulo 4 equals 0, then it's a leap year, if the year % 4 = 0 and year % 100 = 0 then it's not. And finally, if the year % 4 = 0 and year % 100 = 0 and year % 400 = 0, then it is.

Here's the code :

 public static boolean isLeapYearGregorian(int year) {
    if ((year % 4 == 0) && (year % 100 != 0) || (year % 4 == 0) && (year % 100 == 0) && (year % 400 == 0)) {
        return true;
    }
    else {
        return false;
    }

}

Thanks

Observation: the fragment `(year % 4 == 0) && (year % 100 == 0) && (year % 400 == 0)` can be simplified to just `(year%400==0)` (since any multiple of 400 is necessarily a multiple of 4 and 100). — khelwood, Nov 30 '16 at 14:48
Check some more years. Does it work for 2016? 2017? 1600? 1601? The more cases you test, the more your confidence can grow. This is the essence of unit testing. If you're still unsure, ask yourself why, and if your doubts are reasonable then come up with more test cases to assuage them. — John Kugelman, Nov 30 '16 at 14:48

tar · Answer 1 · 2017-05-20T01:50:34.083

For the record, the code can be written as simply

public static boolean isLeapYearGregorian(int year) {
  return (year % 4 == 0) && (year % 100 != 0) || (year % 400 == 0);
}

But for the sake of starting close to the OP's code, let's begin with this:

public static boolean isLeapYearGregorian(int year) {
  return (year % 4 == 0) && (year % 100 != 0) || (year % 4 == 0) && (year % 100 == 0) && (year % 400 == 0);
}

At this point, you need to know the operator precedence in Java, because the ands (&&) and ors (||) above are at the same level, and it makes a difference. Short answer: AND comes before OR.

Now the logic can be listed as:

(year % 4 == 0) AND (year % 100 != 0)
OR
(year % 4 == 0) AND (year % 100 == 0) AND (year % 400 == 0)

Which is to say:

(year divisible by 4) AND (year not divisible by 100)
OR
(year divisible by 4) AND (year divisible by 100) AND (year divisible by 400)

Now you can compare the logic with the pseudocode of the definition of a Gregorian calendar leap year:

if (year is not divisible by 4) then (it is a common year)
else if (year is not divisible by 100) then (it is a leap year)
else if (year is not divisible by 400) then (it is a common year)
else (it is a leap year)

From here it is straightforward to compare to the logic we extracted from the code in your question, and verify that yes the code correctly identifies leap years, as defined by Wikipedia.

If the comparison doesn't seem all that "straightforward", you can resort to truth tables, and prove exhaustively that the two logical statements are the same.

Proving that this code is finding if the year is a leap year

1 Answers1