Dafny: копировать область области метод валидация

Question

Я работаю над языковым сопоставлением нескольких языков, созданных с учетом верификации (в то время, когда Дайни и Фрама-С и т. Д.) Мне был дан этот пример функции, которая скопировала область одного массив в другой массив с различным размещением внутри целевого массива. Спецификация я придумал внешний вид, как это в 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 

Answer 1

Вы можете получить его, чтобы проверить, добавив еще один инвариант

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; 
    } 
}