如何归纳映射集或...？

Question

致力于验证计数反转算法的版本。我觉得pairMapSize 拥有它需要的一切，但它却超时了。我可以尝试对数组的切片进行归纳，但我需要定义一个函数来生成另一个集合，例如从 (xs[0], YY) 开始的所有反转的集合，但这只是另一种比较的情况设置尺寸。

    predicate IsInverted(xs: seq<int>, i: int, j: int) {
        0 <= i < j < |xs| && xs[i] > xs[j]
    }

    function inversionSet(xs: seq<int>): set<(int,int)> {
        set i,j | 0 <= i < j < |xs| && IsInverted(xs, i, j) :: (i,j)
    }

    function pairSetMap(ss: set<(int, int)>, i: int): set<(int, int)> 
    {
        set pair | pair in ss :: (pair.0 + i, pair.1 + i)
    }

    lemma {:verify } {:timelimit 30} {:vcs_split_on_every_assert} pairMapSize(xs: seq<int>, i: int)
        requires 0 <= i
        ensures |pairSetMap(inversionSet(xs), i)| == |inversionSet(xs)|
    {
        if inversionSet(xs) == {} {
            assert |inversionSet(xs)| == 0;
            assert pairSetMap(inversionSet(xs), i) == {};
            assert |pairSetMap(inversionSet(xs), i)| == 0;
        }else{
            // forall x | x in inversionSet(xs)
            //     ensures (x.0+i, x.1+i) in pairSetMap(inversionSet(xs), i)
            // {

            // }

            // forall x | x in pairSetMap(inversionSet(xs), i)
            //     ensures (x.0-i, x.1-i) in inversionSet(xs)
            // {

            // }
            var ixs := inversionSet(xs);
            var pxs := pairSetMap(inversionSet(xs), i);
            var x :| x in inversionSet(xs);
            assert (x.0+i, x.1+i) in pxs;
            assert |ixs| == 1 + |ixs-{x}|;
            assert |pxs| == 1 + |pxs-{(x.0+i, x.1+i)}|;
            var removed: set<(int, int)> := {};
            var premoved: set<(int, int)> := {};
            var mixs := 0;
            var mpxs := 0;
            while ixs != {} 
                invariant ixs == inversionSet(xs)-removed
                invariant ixs <= inversionSet(xs)
                invariant ixs !! removed
                invariant pxs == pairSetMap(inversionSet(xs), i)-premoved
                invariant pxs <= pairSetMap(inversionSet(xs), i)-premoved
                invariant pxs !! premoved
                invariant forall x :: x in removed ==> (x.0+i, x.1+i) in premoved
                invariant forall x :: x in premoved ==> (x.0-i, x.1-i) in removed
                invariant mixs == |removed|
                invariant mpxs == |premoved|
                invariant mixs == mpxs
            {
                var x :| x in ixs;
                assert x !in removed;
                var mx := (x.0+i, x.1+i);
                assert mx !in premoved by {
                    if mx in premoved {
                        assert x in removed;
                        assert false;
                    }
                }
                assert mx in pxs;
                ixs := ixs - {x};
                pxs := pxs - {mx};
                mixs := mixs + 1;
                mpxs := mpxs + 1;
                removed := removed + {x};
                premoved := premoved + {mx};
            }
            assert ixs == {};
            assert pxs == {};
            assert removed == inversionSet(xs);
            assert premoved == pairSetMap(inversionSet(xs), i);
            calc {
                |inversionSet(xs)|;
                |removed|;
                mixs;
                mpxs;
                |premoved|;
                |pairSetMap(inversionSet(xs), i)|;
            }

        }

Answer 1

这个答案没有解释为什么上面的代码无法验证，而是我可以验证的替代解决方案。我在过程中发现了它 编写

pairSetMap

的递归定义。如果我删除了第一个后置条件并仅保留大小后置条件，那么一些想法将表明，如果

(s.0 + i, s.1 + i)

已经存在，则后置条件不一定成立 在

pairSetMap(ss - {i})

。这促使我写了第一个帖子条件。现在所有 它需要的是其他部分的一些断言。

predicate IsInverted(xs: seq<int>, i: int, j: int) {
    0 <= i < j < |xs| && xs[i] > xs[j]
}

function inversionSet(xs: seq<int>): set<(int,int)> {
    set i,j | 0 <= i < j < |xs| && IsInverted(xs, i, j) :: (i,j)
}

method pairSetMap(ss: set<(int, int)>, i: int) returns (r: set<(int, int)>) 
  ensures forall p :: p in ss <==> (p.0 + i, p.1 + i) in r
  ensures |r| == |ss|
{
    if |ss| < 1 {
      r := set pair | pair in ss :: (pair.0 + i, pair.1 + i);
    }
    else { 
        var s :| s in ss;
        var t := pairSetMap(ss - {s}, i);
        assert |t| == |ss - {s}|;
        assert |ss| == |ss - {s}| + 1;
        assert (s.0 + i, s.1 + i) !in t by {
           if (s.0 + i, s.1 + i) in t {
                assert (s.0, s.1) in ss - {s};
                assert (s.0, s.1) !in ss - {s};
           }
        }
        r := t + { (s.0 + i, s.1 + i) };
        assert |r| == |t| + 1;
    }
}