gpt4 book ai didi

formal-verification - 如何提示 Dafny 对序列进行归纳?

转载 作者:行者123 更新时间:2023-12-02 03:16:38 27 4
gpt4 key购买 nike

我想知道我需要在以下内容中添加什么才能让它通过 dafny?

function mapper (input: seq<int>) : seq<(int, int)>
ensures |mapper(input)| == |input|
{
if |input| == 0 then []
else [(0,input[0])] + mapper(input[1..])
}

// given [(0,n1), (0,n2) ... ] recovers [n1, n2, ...]
function retList (input: seq<(int, int)>, v : int) : seq<int>
ensures |input| >= |retList(input, v)|
ensures forall i :: 0 <= i < |input| && input[i].0 == v ==> input[i].1 in retList(input, v)
ensures forall x,y : int :: (x,y) in input && x == v ==> y in retList(input, v)
{
if input == [] then []
else if input[0].0 == v then [input[0].1] + retList(input[1..], v)
else retList(input[1..], v)
}


method test (input: seq<int>)
requires |input| > 0
{
assert retList(mapper(input), 0) == input;
}

最佳答案

编辑(我之前的回答不准确):我认为因为归纳涉及到 input 序列,所以 Dafny 不能自己进行归纳。您编写的代码中没有任何地方会提示 Dafny 的归纳试探法尝试对 input 进行归纳。

所以你需要写a lemma with input as an argument ,当你这样做时,Dafny 会猜测对论证的归纳可能会有帮助,然后将能够自动进行。您实际上并不需要您添加的任何规范。

function mapper (input: seq<int>) : seq<(int, int)>
{
if |input| == 0 then []
else [(0,input[0])] + mapper(input[1..])
}

lemma allKeysRetainsInput(input: seq<int>)
ensures retList(mapper(input), 0) == input
{ }

// given [(v,n1), (v+1,n2), (v,n3), ... ] recovers [n1, n3,...]
function retList (input: seq<(int, int)>, v : int) : seq<int>
{
if input == [] then []
else if input[0].0 == v then [input[0].1] + retList(input[1..], v)
else retList(input[1..], v)
}

method test (input: seq<int>)
requires |input| > 0
{
allKeysRetainsInput(input);
assert retList(mapper(input), 0) == input;
}

如果您想查看更多证明,可以关闭该引理的自动归纳。然后你将需要手动调用归纳假设

lemma {:induction false} allKeysRetainsInput(input: seq<int>)
ensures retList(mapper(input), 0) == input
{
if input != [] {
allKeysRetainsInput(input[1..]);
}
}

关于formal-verification - 如何提示 Dafny 对序列进行归纳?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36667903/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com