Dafny - реализация подстановки

Question

Im пытается написать простую проверенную реализацию метода подстроки. Мой метод принимает 2 строки и проверяет, находится ли str2 в str1. Im пытается выяснить во-первых, почему мой invairant не держит - Dafny отмечает, что инвариант может не удержаться на входе, и пока мои условия pre/post терпят неудачу. Мои мысли об invairant заключаются в том, что есть 3 основных сценария: 1. Петле не удалось найти подстроку в индексе i, и для изучения будет найдено больше индексов. 2. Цикл не смог найти подстроку по индексу i - больше индексов исследовать 3. петля найдено подстроки по индексу я

Код:

method Main() { 
    var str1,str2 := "Dafny","fn"; 
    var found,offset := FindSubstring(str1,str2); 
    assert found by 
    { 
     calc { 
      str2 <= str1[2..]; 
     ==> 
      IsSubsequenceAtOffset(str1,str2,2); 
     ==> 
      IsSubsequence(str1,str2); 
     == 
      found; 
     } 
    } 
    assert offset == 2 by 
    { 
     assert found && str2 <= str1[2..]; 
     assert offset != 0 by { assert 'D' == str1[0] != str2[0] == 'f'; } 
     assert offset != 1 by { assert 'a' == str1[1] != str2[0] == 'f'; } 
     assert offset != 3 by { assert 'n' == str1[3] != str2[0] == 'f'; } 
     assert !(offset >= 4) by { assert 4 + |str2| > |str1|; } 
    } 
    print "The sequence "; 
    print str2; 
    print " is a subsequence of "; 
    print str1; 
    print " starting at element "; 
    print offset; 
} 

predicate IsSubsequence<T>(q1: seq<T>, q2: seq<T>) 
{ 
    exists offset: nat :: offset + |q2| <= |q1| && IsSubsequenceAtOffset(q1,q2,offset) 
} 

predicate IsSubsequenceAtOffset<T>(q1: seq<T>, q2: seq<T>, offset: nat) 
{ 
    offset + |q2| <= |q1| && q2 <= q1[offset..] 
} 

predicate Inv<T>(str1: seq<T>, str2: seq<T>, offset: nat, found: bool) 
{ 
    |str1| > 0 && |str2| > 0 && |str1| >= |str2| && offset <= |str1|-|str2| && 
    (!found && offset < |str1|-|str2| ==> !(str2 <= str1[offset..])) && 
    (!found && offset == |str1| -|str2| ==> !IsSubsequence(str1, str2)) && 
    (found ==> IsSubsequenceAtOffset(str1, str2, offset)) 
} 

method FindSubstring(str1: string, str2: string) returns (found: bool, offset: nat) 

    requires |str2| <= |str1| 
    ensures found <==> IsSubsequence(str1,str2) 
    ensures found ==> IsSubsequenceAtOffset(str1,str2,offset) 
    { 
    found, offset := str2 <= str1[0..], 0; 
    assert Inv(str1,str2,offset,found); 

    while !found && offset <= (|str1| - |str2|) 
     invariant Inv(str1,str2,offset,found) 
    { 
     if str2 <= str1[(offset + 1)..] { 
     found, offset := true, offset + 1; 
     } else { 
     offset := offset + 1; 
     } 
    } 
    Lemma(str1,str2,found,offset); 
    } 

    lemma Lemma(str1: string, str2: string, found: bool, offset: nat) 
    requires !(!found && offset <= (|str1| - |str2|)) 
    requires Inv(str1,str2,offset,found) 
    ensures found <==> IsSubsequence(str1,str2) 
    ensures found ==> IsSubsequenceAtOffset(str1,str2,offset) 
    {} 

Ссылка: http://rise4fun.com/Dafny/QaAbU Любая помощь будет оценена.

Answer 1

http://rise4fun.com/Dafny/q9BG

1) в inv|str1| > 0 && |str2| > 0 был неудачу, потому что это условие не добавляется в требовании функции FindSubstring

2) Так как в то время как тело цикла в FindSubstring проверки подстроки для offset+1, цикл пока только должен быть рассчитан на offset < (|str1| - |str2|), потому что, если offset == (|str1| - |str2|), то не существует никакого смещения, которое бы удовлетворяло str2 <= str1[offset..]

3) Добавлено квантор в inv, который гарантирует, что для всех смещений k где 0 <= k <= offset, не существует какой-либо k который str2 <= str1[offset..]

Небольшой совет для отладки неисправной инвариант, который может помочь: заменить inv вызов с реальным телом inv и dafny точно определит условие отказа в инварианте.

Надеюсь, что это имеет смысл.