Следуя нашему предыдущему посту, мы рассмотрим несколько более сложную версию проблема.

Дан массив целых чисел nums и целое число k, вернуть true, если в массиве есть два различных индекса i и j, такие что nums[i] == числа[j] и abs(i — j) <= k.


Реализация

Вот как мы могли бы решить это в 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;
};
Войти в полноэкранный режим

Выйти из полноэкранного режима

Короче говоря, мы снова создаем набор чисел и добавляем к нему элементы массива по мере выполнения итерации. Однако, как только мы прошли мимо k-го индекса, мы начинаем удалять (ik)-е элементы из списка. Если мы делаем это на каждом последующем шаге, это гарантирует, что только последние k элементов массива находятся в наборе, а затем, если мы встречаем элемент, уже в этом наборе, мы знаем, что это дубликат, который находится в позиции индекса x такой, что xi <= к.


Указание реализации

Мы снова преобразуем определение проблемы в пункт спецификации в пункты спецификации в нашем методе Дафни.

Дан массив целых чисел nums и целое число k, вернуть true, если в массиве есть два различных индекса i и j, такие что nums[i] == числа[j] и abs(i — j) <= k.

requires k <= |nums|
ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
Войти в полноэкранный режим

Выйти из полноэкранного режима

Отличие здесь от определения состоит в том, что мы предполагаем, что один индекс i будет меньше, чем другой соответствующий индекс. Таким образом, разность ji всегда будет положительной, поэтому мы можем не использовать абсолютную разность.


Требует

requires — это еще один пункт спецификации, используемый Дафни для наложения ограничений на входные данные, разрешенные для данного метода/функции. В этом случае мы можем прочитать ограничения задачи LeetCode и увидеть, что предоставленное значение k никогда не превышает максимальную длину массива. Таким образом, мы кодируем его как ограничение в нашем методе. Это имеет некоторый логический смысл и в этой задаче.


Проверка реализации

Вот проверочная реализация, которая представляет собой прямое преобразование кода TypeScript.

// {: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;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима


Выбор инвариантов цикла

В отличие от более простой версии задачи у нас есть два режима для нашей переменной цикла iпри этом меньше k и когда он больше или равен k.

В Dafny вы можете указать несколько инвариантов цикла, просто означая, что они являются дополнительными фактами, которые остаются верными по мере повторения цикла.

Здесь мы видим в инварианте цикла, что мы тоже можем написать. Инвариант цикла в виде двух строк с использованием импликации.

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]
Войти в полноэкранный режим

Выйти из полноэкранного режима

Оба определения хороши, но еще один хороший способ справиться со сложными инвариантами — поместить их в функцию-предикат. Часто это хорошая стратегия, которую можно попробовать из-за концепции Триггеры в Dafny, который часто помогает dafny распознавать и доказывать квантификаторы, такие как forall и 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]
}
Войти в полноэкранный режим

Выйти из полноэкранного режима


Предикаты

predicate функции — это подмножество функций Дафни (со всеми вытекающими отсюда свойствами), которые возвращают только логическое значение. В отличие от метода или функции нам не нужно указывать тип возвращаемого значения. Ключевое слово predicate требует, чтобы оно было логическим.

Однако, если мы заменим наши инварианты цикла следующими, Дафни больше не будет проверяться, даже если само тело предикатной функции будет проверяться.

invariant windowSetValid(nums, k, i, windowSet)
Войти в полноэкранный режим

Выйти из полноэкранного режима

Это тот случай, когда автоматическая индукция Дафни падает, и мы должны написать лемму, чтобы объяснить Дафни дополнительные факты.


леммы

lemma похожа на функцию в Dafny, она может принимать параметры с предложениями require и гарантировать, но она существует только в контексте спецификации и не может быть скомпилирована в работающий код. Технически это доказательство.

Здесь мы указываем все, что должно быть истинным, когда мы достигаем положительного случая if в цикле. Затем мы показываем, что если мы предположим, что эти условия истинны, то внутри тела леммы мы покажем, что оно подразумевает истинность условий обеспечения.

Затем мы можем вызвать эту лемму в других методах или функциях или лемме, когда требуемые условия выполняются, и тогда Дафни может показать, что условия гарантии верны. В основном это просто импликация, P(x) ==> Q(x), и P(x) истинно, тогда 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];
    }
}
Войти в полноэкранный режим

Выйти из полноэкранного режима


Утверждать

Одним из наиболее важных инструментов при разработке спецификации Dafny является assert оператор. У этого есть две цели: во-первых, запросить Dafny и посмотреть, что он считает истинным в данной точке спецификации. Во-вторых, он может показать Дафни, что что-то верно, а затем использовать этот факт для других выводов.

Часто используйте assert, чтобы убедиться, что то, что должно быть очевидным, действительно так. Довольно часто Дафни не поверит вам, если вы не докажете, что что-то истинно, используя последовательность утверждений, или вычисление (еще одна синтаксическая конструкция), или лемму.

В приведенной выше лемме мы утверждаем, что выводы предиката windowSetValid верны, а затем Дафни видит, что условие действительно, и наш метод проверяет, когда мы вызываем лемму в методе.

Эта версия метода проверяет с помощью предиката и леммы.


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;
}
Войти в полноэкранный режим

Выйти из полноэкранного режима