1

我正在尝试在 dafny 中编写一个程序，以查找给定整数集的所有子集，其乘积是给定数字。

我所做的是实现 ComputeSubProduct、FindProductSets 和 GenerateAllIndexSubsets 方法。

这是我到目前为止得到的：

method Main() {
    var q := [2,3,4];
    var productSets := FindProductSets(q, 12);
    assert {1,2} in productSets by {
        calc {
            SubProduct(q, {1,2});
        == { LemmaSubProductsOrderIndifference(q, {1,2}, 1); }
            q[1]*q[2];
        ==
            3*4;
        ==
            12;
        }
    }
}

function SubProduct(q: seq<int>, indexSet: set<nat>): int
    requires InRange(q, indexSet)
{
    if |indexSet| == 0 then 1 else var i :| i in indexSet; q[i] * SubProduct(q, indexSet-{i})
}

predicate InRange<T>(q: seq<T>, indexSet: set<nat>)
{
    forall i :: i in indexSet ==> 0 <= i < |q|
}

function AllIndexSubsets<T>(q: seq<T>): (res: set<set<nat>>)
    ensures forall s :: s in res ==> InRange(q, s)
{
    AllSubsets(set i | P(i) && 0 <= i < |q|)
}

predicate P<T>(x: T) { true } // this is helpful only for avoiding a "no triggers found" warning by Dafny

function AllSubsets<T>(s: set<T>): set<set<T>>
{
    set subset: set<T> | P(subset) && subset <= s
}

method FindProductSets(q: seq<int>, num: int) returns (result: set<set<int>>)
    ensures forall indexSet :: indexSet in result <==> indexSet in AllIndexSubsets(q) && SubProduct(q, indexSet) == num


method GenerateAllIndexSubsets<T>(q: seq<T>) returns (res: set<set<nat>>)
    ensures res == AllIndexSubsets(q)
{
    res := A(q, 0);
}
method A<T>(q: seq<T>, index: nat) returns (res: set<set<nat>>)
    ensures res == AllIndexSubsets(q)
{
    if |q| == 0
        { 
        assert |q| == 0;// if's guard
        // ==>
        assert {} == AllIndexSubsets<nat>([]);
        assert q == [];
        assert {} == AllIndexSubsets(q);
        res := {};
        assert res == AllIndexSubsets(q); // postcondition
        }
    else
        { 
            assert |q| != 0; // !(if's guard)
            var res0 : set<set<nat>> := A(q[1..], index + 1);
            assert res0 == AllIndexSubsets(q[1..]);
            res := res0;    
            assert res ==  AllIndexSubsets(q[1..]); //GenerateAllIndexSubsets postcondition with q[1..]
            //var res1 : set<set<nat>> := AllIndexSubsetsIntersection(q, q[0], res0);
            var res1: set<set<nat>> := (set x | x in res0 :: x + {index});
            assert res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..]);
            assert res0 == AllIndexSubsets(q[1..]);
            assert res1 == AllIndexSubsets(q) - res0;
            // ==>
            assert res0 + res1 == AllIndexSubsets(q);
            res := res + res1;
            assert res == AllIndexSubsets(q); // postcondition
        }
    assert res == AllIndexSubsets(q); // postcondition
} 


method ComputeSubProduct(q: seq<int>, indexSet: set<nat>) returns (prod: int)
    requires InRange(q, indexSet)
    ensures prod == SubProduct(q, indexSet)

lemma {:verify false} LemmaSubProductsOrderIndifference(q: seq<int>, indexSet: set<nat>, i: nat)
    requires i in indexSet
    requires InRange(q, indexSet)
    ensures q[i] * SubProduct(q, indexSet-{i}) == SubProduct(q, indexSet)
{}

我在“A”方法中遇到断言违规：

  1. 断言 {} == AllIndexSubsets([])
  2. 断言 res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..])
4

1 回答 1

2

这两种说法都是错误的。

  1. 空集是 的成员AllIndexSubsets([])，因为空集是任何集合的子集。

  2. AllIndexSubsets(q) - AllIndexSubsets(q[1..]){0, ..., |q|-1}由包含的所有子集组成|q|-1。但由包含res1的所有子集组成。{0, ..., |q|-2}index

一些进一步的评论。

您应该小心使用表达式AllIndexSubsets(q[1..])，因为它将返回一组索引到q[1..]，在使用时q将“关闭一个”。例如，q[1..][0]是q[1]，不是q[0]。换句话说，in的索引q[1..]从对应的索引“移一”到q。在我看来，您目前没有正确处理此问题。

你的使用index是相当神秘的。它是该方法的参数，因此采用任意值（因为它不受前提条件的约束）。但是你使用它好像（粗略地说）它等于|q|-1. 这里也有些可疑。

于 2018-02-26T17:31:07.120 回答