4
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ Yes, there is a generic approach. Use Hoare logic. $\endgroup$ – Kai May 27 '18 at 11:12
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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