Verifying Leetcode question 2176. Count Equal and Divisible Pairs in an Array
Let's take a look at this leetcode problem.
We are asked to count pairs of indices, i and j where i < j, in the provided array that are equal and when multiplying them together are divisible by some integer k.
It is a fairly straight forward problem to solve but how do we prove that our solution is correct?
function countPairs(nums: number[], k: number): number {
let count = 0;
for(let i = 0; i < nums.length-1; i++) {
for(let j = i+1; j < nums.length; j++) {
if(nums[i] == nums[j] && (i*j) % k == 0) {
count++;
}
}
}
return count;
}
First we define our functions and predicates that we can use to define our intended goal. We encapsulate the condition we are checking for as a predicate function. Predicates in Dafny are just functions which return a boolean and they are ubiquitous which is why they get their own keyword. Quite often when you define the right predicate many things fall into place easily for verifying programs.
Then we define the pairs function which returns a set which is basically as simple of a description of the intended goal as possible.
predicate satPairs(nums: seq<nat>, k: nat, a: nat, b: nat)
requires k > 0
requires a < b < |nums|
{
nums[a] == nums[b] && (a*b) % k == 0
}
function pairs(nums: seq<nat>, k: nat): set<(int, int)>
requires k > 0
{
set x, y | 0 <= x < y < |nums| && satPairs(nums, k, x, y) :: (x,y)
}
The set notation of Dafny follows the convention of most math texts, where we can read it as saying the set of pairs (x,y) where x is less than y, and both are less than the length of nums and x and y satisfy the conditions for a pair.
Our specification of the problem begins like this.
method countPairs(nums: seq<nat>, k: nat) returns (count: nat)
requires k > 0
requires |nums| >= 2
ensures count == |pairs(nums,k)|
{
}
One issue with Dafny that beginners will run into is that it will not automatically determine the cardinality (aka the size) of a set. It really only focuses on if an item is or is not in a set. The size of a set must be determined inductively either with a lemma or in a method.
Similarly, when using a for or while loop some incremental progress is being made towards the goal. You need to show that inductively it builds towards your goal. To that end we can define two different helper functions to define what partial progress means in this problem.
PairsI represents all possible pairs that are less than the current i in the loop. In Dafny ghost variables are variables which do not exist at execution time but are there to help verify the intend properties. In this case we define cpairs to represent the set of pairs that we are building up.
function pairsI(nums: seq<nat>, k: nat, i: nat): set<(nat, nat)>
requires k > 0
requires 0 <= i < |nums|
{
set x: nat, y:nat | 0 <= x < i && x < y < |nums| && satPairs(nums, k, x, y) :: (x,y)
}
method countPairs(nums: seq<nat>, k: nat) returns (count: nat)
requires k > 0
requires |nums| >= 1
ensures count == |pairs(nums,k)|
{
count := 0;
ghost var cpairs: set<(nat, nat)> := {};
for i : nat := 0 to |nums|-1
invariant cpairs == pairsI(nums, k, i)
invariant count == |pairsI(nums, k, i)|
{
}
}
In the original program we had an inner for loop and we need to track the progress of that as well. The function pairsJ builds the set of pairs that match for the current i iteration of the outer loop and the jth iteration of the inner loop.
function pairsJ(nums: seq<nat>, k: nat, i: nat, j: nat): set<(nat, nat)>
requires 0 <= i < |nums|
requires i < j
requires k > 0
{
set x: nat | i < x < j <= |nums| && satPairs(nums, k, i, x) :: (i,x)
}
method countPairs(nums: seq<nat>, k: nat) returns (count: nat)
requires k > 0
requires |nums| >= 1
ensures count == |pairs(nums,k)|
{
count := 0;
ghost var cpairs: set<(nat, nat)> := {};
for i : nat := 0 to |nums|-1
invariant cpairs == pairsI(nums, k, i)
invariant count == |pairsI(nums, k, i)|
{
ghost var occount := count;
ghost var increment := 0;
ghost var pairset: set<(nat, nat)> := {};
for j := i+1 to |nums|
invariant i+1 <= j <= |nums|
invariant pairset == pairsJ(nums,k, i,j)
invariant increment == |pairsJ(nums,k,i,j)|
invariant count == occount + increment
{
if satPairs(nums, k, i, j) {
increment := increment + 1;
pairset := pairset+{(i,j)};
count := count + 1;
}
}
cpairs := cpairs + pairset;
}
assert pairsI(nums,k, |nums|-1) == pairs(nums,k);
}
An important consideration in Dafny is that we can show pairsI(nums, k, i) + pairsJ(nums, k, i, |nums|) is equivalent to pairsI(nums, k, i+1).
We can show this with a lemma. Which Dafny immediately verifies.
lemma PairsIMaintenance(nums: seq<nat>, k: nat, i: nat)
requires k > 0
requires 0 <= i <= |nums|-2
ensures pairsI(nums, k, i+1) == pairsI(nums, k, i)+pairsJ(nums, k, i, |nums|)
{
}
Top comments (0)