# 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 < 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?

• Yes, there is a generic approach. Use Hoare logic.
– Kai
May 27, 2018 at 11:12

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.