Verify LeetCode Question: 219. Contains Duplicate II

Following from our last post, we look at slightly more complicated version of the problem.

Given an integer array nums and an integer k, return true if there are two distinct indices i and j in the array such that nums[i] == nums[j] and abs(i - j) <= k.

An implementation

Here is how we might solve this in JavaScript/TypeScript.

function containsNearbyDuplicate(nums: number[], k: number): boolean {
    let windowSet: Set<number> = new Set();
    const n = nums.length;
    if(k == 0) return false;
    for(let i = 0; i < n; i++) {
        if(windowSet.has(nums[i])) {
            return true;
        }
        if(i >= k) {
            windowSet.delete(nums[i-k]);
        }
        windowSet.add(nums[i]);
    }
    return false;
};

In short, we create a set of numbers again and add elements of the array to it as we iterate. However, once we have moved past the k-th index then we start removing the (i-k)-th elements from the list. If we do this every subsequent step it ensures that only the last k array elements are in the set and then if we encounter an element already in that set we know that it is a duplicate which is in an index position x such that x-i <= k.

Specifying the implementation

Again we convert the problem definition into the specification clause into specification clauses on our Dafny method.

Given an integer array nums and an integer k, return true if there are two distinct indices i and j in the array such that nums[i] == nums[j] and abs(i - j) <= k.

requires k <= |nums|
ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]

The difference here from the definition is that we assume one index i will be less than the than the other matching index. Thus the difference j-i will always be positive, so we can skip using the absolute difference.

Requires

requires is another specification clause used by Dafny to impose limits on the inputs allowed for a given method/function. In this case we can read the LeetCode problem constraints and see that the value k provided never exceeds the maximum length of the array. Thus we encode it as a constraint in our method. It makes some logical sense as well in this problem.

Verifying the implementation

Here is a verifying implementation which is a straight forward conversion of the TypeScript code.

// {:verify true} is an attribute that lets us toggle 
//verifying the method until we are ready
method {:verify  true} containsNearbyDuplicate(nums: seq<int>, k: nat) returns (containsDuplicate: bool) 
    requires k <= |nums|
    ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
{
    var windowSet: set<int> := {};
    if k == 0 {
        return false;
    }

    for i: nat := 0 to |nums| 
        invariant i < k ==> forall x :: x in windowSet ==> x in nums[0..i] 
        invariant i >= k ==> forall x :: x in windowSet ==> x in nums[i-k..i]
        // invariant if i < k then forall x :: x in windowSet ==> x in nums[0..i] else forall x :: x in windowSet ==> x in nums[i-k..i]

    {
        if nums[i] in windowSet {
            return true;
        }
        windowSet := if i >= k then (windowSet -{nums[i-k]}) + {nums[i]} else windowSet + {nums[i]};
    }
    return false;
}

Loop invariants choices

Unlike the simpler version of the problem we have two regimes for our loop variable i, while it is less than k and when it is greater than or equal to k.

In Dafny you can specify multiple loop invariants, simply meaning they are additional facts that remain true as a loop iterates.

Here we can see in the loop invariant that we can write either. The loop invariant as two lines using implication.

invariant i < k ==> forall x :: x in windowSet ==> x in nums[0..i] 
invariant i >= k ==> forall x :: x in windowSet ==> x in nums[i-k..i]

Or

invariant if i < k then forall x :: x in windowSet ==> x in nums[0..i] else forall x :: x in windowSet ==> x in nums[i-k..i]

These are both good definitions, but another good way to deal with complicated invariants is to move them into a predicate function. This is often a good strategy to try because of the concept of Triggers in Dafny, which often helps dafny recognize and prove quantifier expressions, like forall and exists.

predicate windowSetValid(nums: seq<int>, k: nat, i: nat, windowSet: set<int>) 
    requires 0 <= i <= |nums|
    requires 0 < k <= |nums|
{
    if i < k then forall x :: x in windowSet ==> x in nums[0..i]
    else forall x :: x in windowSet ==> x in nums[i-k..i]
}

Predicates

predicate functions are a subset of Dafny functions (with all the properties that entails) that only return a boolean value. Unlike a method or a function we do not need to specify a return type. The predicate keyword demands it be a bool.

However, if we replace our loop invariants with the following Dafny will no longer verify, even though the predicate function body on its own will verify.

invariant windowSetValid(nums, k, i, windowSet)

This is a case where Dafny's automatic induction fall down and we have to write a lemma to explain additional facts to Dafny.

Lemmas

lemma is like a function in Dafny, it can take parameters with require and ensure clauses, but it is only existing within the specification context and cannot be compiled to running code. It is technically a proof.

Here we specify all the things which should be true when we reach the positive if case in the loop. Then we show that if we assume those conditions are true then inside the lemma body we show that it implies the ensure clauses is true.

We can then call that lemma in other methods or functions or lemma when the required conditions are met and then Dafny can show that the ensure conditions are valid. This is basically just implication, P(x) ==> Q(x), and P(x) is true then Q(x).

lemma windowSetValidIsSufficient(nums: seq<int>, k: nat, i: nat, windowSet:set<int>)  
    requires 0 <= i < |nums|
    requires 0 < k <= |nums|
    requires windowSetValid(nums, k, i, windowSet)
    requires nums[i] in windowSet
    ensures exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
{
    if i < k {
        assert nums[i] in windowSet;
        assert forall x :: x in windowSet ==> x in nums[0..i];
    }else{
        assert nums[i] in windowSet;
        assert forall x :: x in windowSet ==> x in nums[i-k..i];
    }
}

Assert

One of the most important tools in developing a Dafny specification is the assert operator. This has two purposes, the first is to query Dafny and see what it believes is true at a given point in a specification. Secondly, it can show Dafny that something is true and then it can use that fact to make other deductions.

Use assert often to see if what should be obvious actually is. Quite frequently Dafny will not believe you unless you show something is true using a sequence of assertions, or a calculation (another syntax construct), or a lemma.

In the above lemma, we assert the conclusions of the windowSetValid predicate being true and then Dafny sees ensure condition is valid and our method verifies when we call the lemma in the method.

This version of the method verifies using the predicate and lemma.

method {:verify  true} containsNearbyValid(nums: seq<int>, k: nat) returns (containsDuplicate: bool) 
    requires k <= |nums|
    ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
{
    var windowSet: set<int> := {};
    if k == 0 {
        return false;
    }

    for i: nat := 0 to |nums| 
        invariant windowSetValid(nums, k, i, windowSet)
    {
        if nums[i] in windowSet {
            windowSetValidIsSufficient(nums, k, i, windowSet);
            return true;
        }
        windowSet := if i >= k then (windowSet -{nums[i-k]}) + {nums[i]} else windowSet + {nums[i]};
    }
    return false;
}