Dafny и подсчет событий

Question

Я смотрел на использование лемм в Дафни, но мне трудно понять, и, очевидно, приведенный ниже пример не проверяет, вполне возможно, потому что Дафни не видит индукции или что-то вроде лемма для доказательства некоторого свойства счетчика? В принципе, я не знаю, как или что мне нужно определить, чтобы помочь убедить Дафни в том, что подсчет является индуктивным, и т. Д. Некоторые из спецификаций обеспечения и инвариантов не нужны, но это не главное. Кстати, это было проще в SpeC#.

function count(items: seq<int>, item: int): nat 
    decreases |items| 
{ 
    if |items| == 0 then 0 else 
    (if items[|items| - 1] == item then 1 else 0) 
     + count(items[..(|items| - 1)], item) 
} 

method occurences(items: array<int>, item: int) returns (r: nat) 
    requires items != null 
    ensures r <= items.Length 
    // some number of occurences of item 
    ensures r > 0 ==> exists k: nat :: k < items.Length 
        && items[k] == item 
    // no occurences of item 
    ensures r == 0 ==> forall k: nat :: k < items.Length 
        ==> items[k] != item 
    ensures r == count(items[..], item) 
{ 
    var i: nat := 0; 
    var num: nat := 0; 

    while i < items.Length 
    // i is increasing and there could be elements that match 
    invariant num <= i <= items.Length 
    invariant num > 0 ==> exists k: nat :: k < i 
          && items[k] == item 
    invariant num == 0 ==> forall k: nat :: k < i 
          ==> items[k] != item 
    invariant num == old(num) + 1 || num == old(num) 
    invariant num == count(items[..i], item) 
    { 
    if items[i] == item 
     { num := num + 1; } 
    i := i + 1; 
    } 
    return num; 
} 

Answer 1

Я хотел бы использовать определение count на основе вокруг мультимножестве, то все работает:

function count(items: seq<int>, item: int): nat 
    decreases |items| 
{ 
    multiset(items)[item] 
} 

method occurences(items: array<int>, item: int) returns (r: nat) 
    requires items != null 
    ensures r <= items.Length 
    // some number of occurences of item 
    ensures r > 0 ==> exists k: nat :: k < items.Length 
        && items[k] == item 
    // no occurences of item 
    ensures r == 0 ==> forall k: nat :: k < items.Length 
        ==> items[k] != item 
    ensures r == count(items[..], item) 
{ 
    var i: nat := 0; 
    var num: nat := 0; 

    while i < items.Length 
    // i is increasing and there could be elements that match 
    invariant num <= i <= items.Length 
    invariant num > 0 ==> exists k: nat :: k < i 
          && items[k] == item 
    invariant num == 0 ==> forall k: nat :: k < i 
          ==> items[k] != item 
    invariant num == old(num) + 1 || num == old(num) 
    invariant num == count(items[..i], item) 
    { 
    if items[i] == item 
     { num := num + 1; } 
    i := i + 1; 
    } 
    assert items[..i] == items[..]; 
    r := num; 
} 

Я также хотел бы предложить два альтернативных подхода, и другое решение оригинального дизайна.

1. Без изменения реализации, лично я бы, вероятно, написать спецификацию, как это:

   function count(items: seq<int>, item: int): nat 
       decreases |items| 
   { 
       multiset(items)[item] 
   } 
   
   method occurences(items: array<int>, item: int) returns (num: nat) 
       requires items != null 
       ensures num <= items.Length 
       ensures num == 0 <==> item !in items[..] 
       ensures num == count(items[..], item) 
   { 
       num := 0; 
   
       var i: nat := 0; 
       while i < items.Length 
       invariant num <= i <= items.Length 
       invariant num == 0 <==> item !in items[..i] 
       invariant num == count(items[..i], item) 
       { 
       if items[i] == item 
        { num := num + 1; } 
       i := i + 1; 
       } 
       assert items[..i] == items[..]; 
   } 
   

2. Если бы я был принять решение о реализации тоже тогда я бы написал так:

   method occurences(items: array<int>, item: int) returns (num: nat) 
       requires items != null 
       ensures num == multiset(items[..])[item] 
   { 
       num := multiset(items[..])[item]; 
   } 
   

3. Существует способ проверить подлинность оригинала, добавив дополнительное утверждение. NB. Я думаю, что «старый» не делает то, что, по вашему мнению, делает в инварианте цикла.

   function count(items: seq<int>, item: int): nat 
       decreases |items| 
   { 
       if |items| == 0 then 0 else 
       (if items[|items|-1] == item then 1 else 0) 
        + count(items[..|items|-1], item) 
   } 
   
   method occurences(items: array<int>, item: int) returns (r: nat) 
       requires items != null 
       ensures r <= items.Length 
       // some number of occurences of item 
       ensures r > 0 ==> exists k: nat :: k < items.Length 
           && items[k] == item 
       // no occurences of item 
       ensures r == 0 ==> forall k: nat :: k < items.Length 
           ==> items[k] != item 
       ensures r == count(items[..], item) 
   { 
       var i: nat := 0; 
       var num:nat := 0; 
   
       while i < items.Length 
       invariant num <= i <= items.Length 
       invariant num > 0 ==> exists k: nat :: k < i 
             && items[k] == item 
       invariant num == 0 ==> forall k: nat :: k < i 
             ==> items[k] != item 
       invariant num == count(items[..i], item) 
       { 
       assert items[..i+1] == items[..i] + [items[i]]; 
   
       if items[i] == item 
        { num := num + 1; } 
       i := i + 1; 
       } 
       assert items[..i] == items[..]; 
       r := num; 
   }