- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我想知道我需要在以下内容中添加什么才能让它通过 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/
我正在阅读一篇非常愚蠢的论文,它一直在谈论乔托如何定义“形式语义”。 Giotto has a formal semantics that specifies the meaning of mode
在下面的程序中,循环的最后一个不变量验证失败。但是如果我把它作为断言放在 while 循环之前,条件就会验证。如果我添加字段 ia 没有改变,它也会验证。为什么需要这个?读取权限不应该暗示这一点吗?我
任何人都可以清楚地解释什么是完全温和的上下文敏感语法吗? 这些语法是否可用于对自然语言建模? 此外,索引语法、头语法和树语法等语法是否属于轻度上下文敏感语法? 最佳答案 Joshi (1985) 引入
程序可以从 START 分支到 LEFT 或 RIGHT 分支。如何检查 LEFT 分支的执行路径和 RIGHT 分支的另一个执行路径? ------------------------------
你知道任何可以指定上下文相关语法的吗?例如 * 符号指针/乘法歧义解析。我正在寻找能够解决这种歧义的正式语言。我正在寻找的语言应该被很好地指定。 编辑:我正在寻找类似 BNF 的东西,但应该是上下文相
关闭。这个问题需要更多focused .它目前不接受答案。 想改善这个问题吗?更新问题,使其仅关注一个问题 editing this post . 4年前关闭。 Improve this questi
给定一个循环不变式,维基百科列出了一种为循环生成最弱前提条件的好方法(来自 http://en.wikipedia.org/wiki/Predicate_transformer_semantics )
在乔姆斯基的层次结构中,没有定义递归语言集。我知道递归语言是递归可枚举语言的一个子集,并且所有递归语言都是可判定的。 我很好奇递归语言与上下文敏感语言的比较。我可以假设上下文相关语言是递归语言的严格子
我有一项家庭作业,除一个问题外,我已经完成(参见标题) 对于我的一生,我无法弄清楚……所以我开始认为这是一个棘手的问题。 我将提交的当前答案是: L1 = {a^n b^n: n>=1} is det
我正在尝试在 Isabelle 中输入和证明 Z 规范。 假设我有一个用 LaTeX 格式编写的自动售货机规范: \begin{zed} price:\nat \end{zed} \b
我在达夫尼(Dafny)得到警告,说我的量词有 No terms found to trigger on. 我要为代码执行的操作是找到平方值小于或等于给定自然数'n'的最大数字。这是到目前为止我想出的
实际上,我想从 1..N 构建一个 {"1", "2", "3", ..., "N"} 集> 设置。如何将数字转换为字符串? 最佳答案 TLC 模块提供了一个ToString 运算符。 关于forma
考虑解决 100 prisoners and a lightbulb 的标准策略问题。这是我在 Dafny 中对其进行建模的尝试: method strategy(P: set, Special: T
一段时间以来,我一直对形式方法感兴趣。我已经使用正式的方法来推理我一直在从事的一些项目的一些非常具体的子领域。我永远无法说服其他团队成员尝试相同的方法,更不用说用正式的方法指定整个域了。 我发现特别有
感谢 this question 的精彩回复我了解如何使用可变参数调用 javascript 函数。 现在我希望使用与构造函数一起应用 我发现了一些有趣的信息on this post . 但是我的代码
我真的找遍了所有地方,但没有找到我的问题的答案: 一般化问题: 如何在不启动 R 函数的情况下评估 R 函数的参数 (formals())? 尽管 R 的“懒惰评估”,您如何评估 R 中的整个环境?
我想知道我需要在以下内容中添加什么才能让它通过 dafny? function mapper (input: seq) : seq ensures |mapper(input)| == |input|
我正在和 KeY ( https://www.key-project.org ) 一起玩一个教学项目。 一方面,我很高兴 KeY 轻松证明了以下带 jml 注释的 Java 代码的正确性 /*@ en
我真的找遍了所有地方,但没有找到我的问题的答案: 一般化问题: 如何在不启动 R 函数的情况下评估 R 函数的参数 (formals())? 尽管 R 的“懒惰评估”,您如何评估 R 中的整个环境?
这是我要证明的代码: function rec_even(a: nat) : bool requires a >= 0; { if a == 0 then true else if a
我是一名优秀的程序员,十分优秀!