Prove correctness of the iterative algorithm

Question

Description:

Given an array nums and a value val, remove all instances of that value in-place and return the new length.

Do not allocate extra space for another array, you must do this by modifying the input array in-place with O(1) extra memory.

The order of elements can be changed. It doesn't matter what you leave beyond the new length.

Code:

class Solution {
    public int removeElement(int[] nums, int val) {
        int count = 0;
        for (int i = 0; i < nums.length; i++) {
            if (nums[i] != val) {
                nums[count++] = nums[i];
            }
        }
        return count;
    }
}

The problem may seem very simple but the solution I came up with is quite intuitive and hence it may be prone to errors in situations like interviews, I would like to know if there is some sort of formal check for the correctness? if yes then, is there any generic approach?

Answer 1

Let Nums be the value of the array after method execution, and nums the initial value. Let,

P(i) = Nums[0..i-1] is the same as nums[0..i-1], but ignoring `val`.

Your algorithm is correct if P(nums.length) is true. This can be shown by realising that P is true at the beginning of the loop, and each iteration of the loop preserves P.

Initially, i = 0 in the for loop, and we have

   P(0)
 = Nums[0..0-1] is the same as nums[], but ignoring `val`.
 = Nums[] is the same as nums[], but ignoring `val`.
 = true

Next, assuming P(i), for $i \leq nums.length$, show P(i+1) ;-)

---

This is some of the work of the Hoare Calculus mentioned above.