验证循环修改子句

问题描述

是的，所以我正在尝试验证以下 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 特征和 @。