5
$\begingroup$

How can I prove algorithm correctness ? when i face a problem and come up with a solution the only way to know if this a valid solution or not is by trying some test cases. if they pass through the algorithm and produce the expected output then my algorithm most properly true. but obviously this is not hold all the time because i may forget some corner cases or it is hard to figure out all the test cases. So how can I prove mathematically if my algorithm produce the expected output or not ?

For example, consider the program below.

You’re given a read only array of $n$ integers. Find out if any integer occurs more than $n/3$ times in the array in linear time and constant additional space.

Algorithm: We will use an array of size 3 to count occurrence of numbers let it be count adding numbers to our count array with its proper count. If we reach the size of count array we decrement one from count of each number. If number count becomes zero it can be safely eliminated from the count array.

Here is an example:

  • Input: 4 3 3 7 2 3 4 5
  • count arr (4,1) 4 as first element and 1 is its count till now
  • count arr (4,1)(3,1)
  • count arr (4,1)(3,2)
  • count arr (4,1)(3,2)(7,1). Here we reach the max allowed size for count then we need to decrement count by one and if it reaches zero its item will be removed from our count array so count arr becomes count arr (3,1). We will proceed with next element in the array which is 2.
  • count arr (3,1)(2,1)
  • count arr (3,2)(2,1)
  • and so on. At the end count arr will be (3,1)(5,1).

We will make another loop to the input array to count occurrence of 3 and 5 and if any one exceeds $n/3$ it will be printed out.

$\endgroup$

closed as too broad by Yuval Filmus, hengxin, Ran G., D.W., David Richerby Jun 20 '15 at 7:55

Please edit the question to limit it to a specific problem with enough detail to identify an adequate answer. Avoid asking multiple distinct questions at once. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ You will need to tell us what algorithm you have in mind, otherwise your question is way too general. $\endgroup$ – Yuval Filmus Jun 20 '15 at 3:40
  • $\begingroup$ @YuvalFilmus my question is not for specific algorithm, i need a guide line for proofing algorithm correctness. not for a specific one. $\endgroup$ – Mahmoud Emam Jun 20 '15 at 4:45
  • 1
    $\begingroup$ You use mathematical proof. $\endgroup$ – Yuval Filmus Jun 20 '15 at 4:47
  • 1
    $\begingroup$ I believe that Yuval meant that the way to prove depends much on the specific algorithm. There are plenty of methods: by induction, case analysis, etc. etc. Try to search this site within the algorithm tag questions that have "correctness" in their title, you will find several different examples $\endgroup$ – Ran G. Jun 20 '15 at 4:48
  • 1
    $\begingroup$ This is far too broad to answer. It's at essentially the level of "How do I prove a mathematical theorem?" $\endgroup$ – David Richerby Jun 20 '15 at 7:54
10
$\begingroup$

In practice, to prove an algorithm you should search a good invariant property for each loop. For example, if you compute in a given order the sum of $n$ integers with a for loop (indexed by $i$), the invariant could be : "At the end of an iteration, the $sum$ variable contains the sum of the $i$ first values". It's invariant over iterations number and always true, it's easy to prove this by recurrence on the iterations number. Afterwards you can easily conclude that, at the end of the loop, $i=n$ and thus that $sum$ is the expected sum.

Then, there is several levels of strictness, but for simple algorithms we can generally conclude promptly since the correction of the algorithm becomes almost always trivial with all the loops invariants. A very classical approach is to prove before that the algorithm finishes and after that the algorithm is correct when it ends. For complete examples you can look here. For more subtil algorithms, you can also need some mathematical theorems which provide some links beetween objects.

Your example is very close to Misra-Gries algorithm. You can look for the proof of the Misra-Gries algorithm and try to adapt it or you can try to bound the number of times the count of the most frequent number is decreased.

In general, there isn't a systematic way to find if an algorithm produces the expected output or not. Indeed, this systematic way would be an algorithm and such an algorithm can't exist (Rice's theorem).

$\endgroup$
  • $\begingroup$ i found this paper that describe Misra-Gries algorithm is very helpful and i get a clue of why proposed algorithm is correct. $\endgroup$ – Mahmoud Emam Jun 20 '15 at 14:49

Not the answer you're looking for? Browse other questions tagged or ask your own question.