DAFNY:复制阵列区域方法验证[英] Dafny: copy array region method validation

本文是小编为大家收集整理的关于DAFNY:复制阵列区域方法验证的处理方法,想解了DAFNY:复制阵列区域方法验证的问题怎么解决?DAFNY:复制阵列区域方法验证问题的解决办法?那么可以参考本文帮助大家快速定位并解决问题。

问题描述

我正在研究用验证的验证(whery,dafny和frama-c等)​​的语言比较在目标数组中.我在Dafny的说明书看起来像这样:

method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
    returns (r: array<int>)
  // both arrays cannot be null
   requires dest != null && src != null
  // Source array must contain enough elements to be copied
   requires src.Length >= sStart + len
  // Destination array must have enough space for copied elements
   requires dest.Length >= dStart + len
  // Result is same size as dest
  ensures r != null
  ensures r.Length == dest.Length
  // All elements before copied region are same
   ensures r[..dStart] == dest[..dStart]
  // All elements above copied region are same
   ensures r[dStart + len..] == dest[dStart + len..]
  // All elements in copied region match src
   ensures forall k: nat :: k < len ==> r[dStart + k] == src[sStart + k]

{
    if len == 0 { return dest; }
    assert len > 0;
    var i: nat := 0;
    r := new int[dest.Length];
    while (i < r.Length)
      invariant i <= r.Length
      decreases r.Length - i
      invariant r.Length == dest.Length
      invariant forall k: nat :: k < i ==> r[k] == dest[k]
    {
        r[i] := dest[i];
        i := i + 1;
    }
    assume r[..] == dest[..];
    i := 0;
    while (i < len)
      invariant i <= len
      decreases len - i
      invariant r.Length == dest.Length
      invariant r.Length >= dStart + i
      invariant src.Length >= sStart + i
      invariant r[..dStart] == dest[..dStart]
      invariant r[(dStart + len)..] == dest[(dStart + len)..]
      invariant forall k: nat :: k < i ==> r[dStart + k] == src[sStart + k]
    {
        r[dStart + i] := src[sStart + i];
        i := i + 1;
    }
}

在第二次上方的循环时可能有一些不需要的不变性,因为我试图涵盖我可以想到的一切.但是,是的,这不会验证,我困惑为什么...

Dafny/copy.dfy(35,4): Error BP5003: A postcondition might not hold on this return path.
Dafny/copy.dfy(17,11): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon19_Else
    Dafny/copy.dfy(24,5): anon20_LoopHead
    (0,0): anon20_LoopBody
    Dafny/copy.dfy(24,5): anon21_Else
    (0,0): anon23_Then
    Dafny/copy.dfy(35,5): anon24_LoopHead
    (0,0): anon24_LoopBody
    Dafny/copy.dfy(35,5): anon25_Else
    (0,0): anon27_Then
Dafny/copy.dfy(43,16): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
    (0,0): anon0
    (0,0): anon19_Else
    Dafny/copy.dfy(24,5): anon20_LoopHead
    (0,0): anon20_LoopBody
    Dafny/copy.dfy(24,5): anon21_Else
    (0,0): anon23_Then
    Dafny/copy.dfy(35,5): anon24_LoopHead
    (0,0): anon24_LoopBody
    Dafny/copy.dfy(35,5): anon25_Else
    Dafny/copy.dfy(35,5): anon27_Else

Dafny program verifier finished with 1 verified, 2 errors

推荐答案

您可以通过添加一个不变性

来验证它.
invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]

如:

while (i < len)
  invariant i <= len
  decreases len - i
  invariant r.Length == dest.Length
  invariant r.Length >= dStart + i
  invariant src.Length >= sStart + i
  invariant r[..dStart] == dest[..dStart]
  invariant r[(dStart + len)..] == dest[(dStart + len)..]
  invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
  invariant forall k: nat :: k < i ==> r[dStart + k] == src[sStart + k]

顺便说一下,如果您想要

,我认为您可以删除许多不变性
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat, len: nat)
    returns (r: array<int>)
  // both arrays cannot be null
   requires dest != null && src != null
  // Source array must contain enough elements to be copied
   requires src.Length >= sStart + len
  // Destination array must have enough space for copied elements
   requires dest.Length >= dStart + len
  // Result is same size as dest
  ensures r != null
  ensures r.Length == dest.Length
  // All elements before copied region are same
   ensures r[..dStart] == dest[..dStart]
  // All elements above copied region are same
   ensures r[dStart + len..] == dest[dStart + len..]
  // All elements in copied region match src
   ensures forall k: nat :: k < len ==> r[dStart + k] == src[sStart + k]

{
    if len == 0 { return dest; }
    var i: nat := 0;
    r := new int[dest.Length];
    while (i < r.Length)
      invariant i <= r.Length
      invariant r[..i] == dest[..i]
    {
        r[i] := dest[i];
        i := i + 1;
    }

    i := 0;
    while (i < len)
      invariant i <= len
      invariant r[..dStart] == dest[..dStart]
      invariant r[(dStart + len)..] == dest[(dStart + len)..]
      invariant r[dStart .. dStart + i] == src[sStart .. sStart + i]
      {
        r[dStart + i] := src[sStart + i];
        i := i + 1;
    }
}

本文地址:https://www.itbaoku.cn/post/1793857.html