Prove correctness of the iterative algorithm 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 &lt; 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?
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.