dafny集成员含义

Question

为下面的这里代码验证另一个简单问题TypeScript。

function containsDuplicate(nums: number[]): boolean {
    let m = new Set();
    for(let elem of nums) {
        if(m.has(elem)) {
            return true;
        }
        m.add(elem);
    }
    return false;
};

我遇到了这样的情况:我可以获得基于setSeq的验证方法，但不能在变量windowSet上进行验证。

function method seqSet(nums: seq<int>, index: nat): set<int> {
    set x | 0 <= x < index < |nums| :: nums[x]
}

method containsDuplicateI(nums: seq<int>) returns (containsDuplicate: bool)
    ensures containsDuplicate ==>  exists i,j :: 0 <= i < j < |nums| && nums[i] == nums[j]
{
    var windowGhost: set<int> := {};
    var windowSet: set<int> := {};
    for i:= 0 to |nums| 
        invariant 0 <= i <= |nums|
        invariant forall j :: 0 <= j < i < |nums|  ==> nums[j] in windowSet
        invariant forall x :: x in windowSet ==> x in nums
        invariant seqSet(nums, i) <= windowSet
    {
        windowGhost := windowSet;
        // if nums[i] in windowSet { // does not verify
        if nums[i] in seqSet(nums, i) { //verifies
            return true;
        }
        windowSet := windowSet + {nums[i]};
    }
    return false;
}

似乎是因为更新了窗口集，所以它不能等同于seqSet的结果，至少断言失败。如何更改不变量，以便可以使用非鬼变量中的成员资格测试而不是函数集来验证该方法？

Answer 1

在将invariant forall x :: x in windowSet ==> x in nums更改为invariant forall x :: x in windowSet ==> x in nums[0..i]之后，我可以验证。