如何解决验证循环修改子句
是的,所以我正在尝试验证以下 fill()
方法。目前第一个和第三个 invariant
子句失败,我不完全确定为什么。任何想法表示赞赏!
class List {
var data : int;
var next : List?;
ghost var rep : set<List>;
constructor(d : int)
ensures this.valid();
{
this.data := d;
this.next := null;
this.rep := {this};
}
predicate valid()
reads this,rep;
decreases rep + {this};
{
this in rep
&& (next != null ==> (
next in rep
&& next.rep <= rep
&& this !in next.rep
&& next.valid()
))
}
}
method fill(ol : List,on : int)
requires ol.valid();
requires on >= 0;
modifies ol.rep;
{
assert ol in ol.rep;
var n := on;
var l : List? := ol;
//
//
while(n >= 0 && l != null)
invariant ol.valid();
invariant (l != null) ==> l.valid();
invariant (l != null) ==> (l in ol.rep);
modifies l.rep;
{
l.data := n;
l := l.next;
n := n - 1;
}
}
解决方法
这是一种方法。
class List {
var data : int;
var next : List?;
ghost var rep : set<List>;
constructor(d : int)
ensures valid()
{
data := d;
next := null;
rep := {this};
}
predicate valid()
reads this,rep
decreases rep + {this}
{
&& this in rep
&& (next != null ==>
&& next in rep
&& next.rep <= rep
&& this !in next.rep
&& next.valid())
}
static twostate lemma valid_frame(a: List)
requires old(a.valid())
requires forall x | x in old(a.rep) :: unchanged(x`next)
requires forall x | x in old(a.rep) :: unchanged(x`rep)
decreases old(a.rep)
ensures a.valid()
{}
}
method fill(ol : List,on : int)
requires ol.valid()
requires on >= 0
modifies ol.rep
ensures ol.valid()
{
var n := on;
var l : List? := ol;
label L:
while(n >= 0 && l != null)
invariant l != null ==> l.valid()
invariant l != null ==> l.rep <= old(ol.rep)
modifies ol.rep`data
{
l.data := n;
l := l.next;
n := n - 1;
}
List.valid_frame@L(ol);
}
这个证明的基本思想是,valid
谓词只依赖于 next
的 rep
和 List
字段。由于 fill
仅写入 data
字段,因此它必须保持有效性。
为了实现这个想法,我们可以在 Dafny 中使用 twostate
引理。将特定旧状态“传递”给此类引理的方法是结合使用 label
特征和 @
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。