We use cookies to ensure you have the best browsing experience on our website. Please read our cookie policy for more information about how we use cookies.
In order to understand why the algo written by Conor Kosidowski is indeed correct, I added the formal analysis of the algo, that uses the loop invariant technique (following the CLRS book) to prove that the algo is indeed correct.
Loop invariant statement: both (a) and (b) below are true.
a) If "sum" is even, then "count" yields the correct number of loaves
to distribute among [ 0, next(i) ) ; true otherwise.
b) If the "sum" is odd, then "count" shows the correct number of loaves
to distribute into the line [ 0, next(i) ], assuming B[next(i)] is odd;
and true otherwise.
Conventions: [A,B) denotes sequence of integers from A to B, excluding B.
Checking the Initialization, Maintenance and Termination requirements:
Initialization (checked just before first iteration):
We need to check tha the loop invariant is true at this time.
Indeed: we have next(i) = 0, hence [0,i) = [0,0) = [], - the
line is empty. The sum is even, and count= 0 reflects
correct number of loaves to distribute.
Maintenance (checked just before each iteration):
Let us check loop the invariant statements
1. Suppose "sum" is even.
We know count = previous(count) in this case.
We need to prove that the count yields correct
number of loaves to distibute in [0,next("i")).
1.1) If "element" is even, then we know, the previous("sum")
is even; Suppose we distribute previous("count") loaves in the
line [0,i), so the requirements are satisfied for [0,i); we know we
can do it by maintenance assumption; Since element is even,
adding this element to line does not break the requirements,
so we conclude the requirements are satisfied for [0,next("i")).
The assertion is proven.
1.2) If element is odd, then we know the previous("sum") is odd,
and by maintenance assumption, we know that
the previous("count") (which is equal to the current value
of count) yields the correct value of loaves to distribute
in [0,next(previous("i"))] = [0,i] = [0,next(i)), assuming B[i]
is odd which is indeed the case. Hence previous("i") which
is equal to current "count", yields correct number of
loaves to distibute in [0,next("i")).
The assertion is proven.
2. Suppose "sum" is odd
We know count = previous(count)+2 in this case
Need to show: "count" shows the correct number of loaves
to distribute into the line [ 0, next(i) ], assuming B[next(i)] is
odd;
2.1. If "element" is even, then we know, the previous("sum")
is odd;
By maintenance assumption previous(count) shows the
correct number of loaves to distribute into the
line [ 0, previous(next(i)) ) = [0,i), extended by one
more participant holding an odd number of loaves.
We need two more loaves if we extend with even
numbered element=B[i] and then with odd
numbered B[next(i)], hence we need previous(count)+2 = count.
The assertion if proven.
2.2 If "element" is odd, then we know previous("sum") is even.
By maintenance assumption, previous("count") is the
correct number of loaves to distribute to
[0,next(previous("i")) = [0,i). Extending with the present odd
numbered element and yet another odd element will require
two more loaves. The assertion is proven.
Termination (checked prior to terminating iteration):
We terminate when next(i) = n
At this time, if sum is even, then by loop invariant, the count
yield the correct # of loaves to distribute in [0,next(i)) = [0,n).
If sum is odd, then we know loaves cannot be distributed,
so the answer is "N0"
Cookie support is required to access HackerRank
Seems like cookies are disabled on this browser, please enable them to open this website
Fair Rations
You are viewing a single comment's thread. Return to all comments →
In order to understand why the algo written by Conor Kosidowski is indeed correct, I added the formal analysis of the algo, that uses the loop invariant technique (following the CLRS book) to prove that the algo is indeed correct.
Loop invariant statement: both (a) and (b) below are true.
a) If "sum" is even, then "count" yields the correct number of loaves to distribute among [ 0, next(i) ) ; true otherwise.
b) If the "sum" is odd, then "count" shows the correct number of loaves to distribute into the line [ 0, next(i) ], assuming B[next(i)] is odd; and true otherwise.
Conventions: [A,B) denotes sequence of integers from A to B, excluding B.
Checking the Initialization, Maintenance and Termination requirements:
Initialization (checked just before first iteration):
Maintenance (checked just before each iteration):
Termination (checked prior to terminating iteration):