Поиск меры прекращения поиска и замены в Дафни?

Question

Я кодирую a search and replace method, который использует методы поиска, удаления и вставки. Я вызываю эти три метода в то время, и я не уверен, о каких предварительных условиях я должен использовать. Любая помощь будет оценена по достоинству.

Полный код:

 method searchAndReplace(line:array<char>, l:int, 
     pat:array<char>, p:int, 
     dst:array<char>, n:int)returns(nl:int) 
     requires line != null && pat!=null && dst!=null; 
     requires !checkIfEqual(pat, dst); 
     requires 0<=l<line.Length; 
     requires 0<=p<pat.Length; 
     requires 0<=n<dst.Length; 

     modifies line; 
     { 
      var at:int := 0; 
      var p:int := n; 

      while(at != -1) 
      invariant -1<=at<=l; 
      { 
      at := find(line, l, dst, n); 
      delete(line, l, at, p); 
      insert(line, l, pat, p, at); 
      } 

      var length:int := line.Length; 

      return length; 
     } 


     function checkIfEqual(pat:array<char>, dst:array<char>):bool 
     requires pat!=null && dst!=null; 
      reads pat; 
     reads dst; 
{ 
    if pat.Length != dst.Length then false 
    else forall i:nat :: i < pat.Length ==> pat[i] == dst[i] 
} 

    // l is length of the string in line 
// p is length of the string in nl 
// at is the position to insert nl into line 
method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int) 
    requires line != null && nl != null 
    requires 0 <= l+p <= line.Length // line has enough space 
    requires 0 <= p <= nl.Length // string in nl is shorter than nl 
    requires 0 <= at <= l // insert position within line 
    modifies line 
    ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i] // ok now 
{ 
    ghost var initialLine := line[..]; 

    // first we need to move the characters to the right 
    var i:int := l; 
    while(i>at) 
    invariant line[0..i] == initialLine[0..i] 
    invariant line[i+p..l+p] == initialLine[i..l] 
    invariant at<=i<=l 
    { 
    i := i - 1; 
    line[i+p] := line[i]; 
    } 

    assert line[0..at] == initialLine[0..at]; 
    assert line[at+p..l+p] == initialLine[at..l]; 

    i := 0; 
    while(i<p) 
    invariant 0<=i<=p 
    invariant line[0..at] == initialLine[0..at] 
    invariant line[at..at+i] == nl[0..i] 
    invariant line[at+p..l+p] == initialLine[at..l] 
    { 
    line[at + i] := nl[i]; 
    i := i + 1; 
    } 

    assert line[0..at] == initialLine[0..at]; 
    assert line[at..at+p] == nl[0..p]; 
    assert line[at+p..l+p] == initialLine[at..l]; 
} 

     method find(line:array<char>, l:int, pat:array<char>, p:int) returns (pos:int) 
    requires line!=null && pat!=null 
    requires 0 <= l < line.Length 
    requires 0 <= p < pat.Length 
    ensures 0 <= pos < l || pos == -1 
{ 
    var iline:int := 0; 
    var ipat:int := 0; 
    pos := -1; 

    while(iline<l && ipat<pat.Length) 
    invariant 0<=iline<=l 
    invariant 0<=ipat<=pat.Length 
    invariant -1 <= pos < iline 
    { 
     if(line[iline]==pat[ipat] && (line[iline]!=' ' && pat[ipat]!=' ')){ 
      if(pos==-1){ 
       pos := iline; 
      } 
      ipat:= ipat + 1; 
     } else { 
     if(ipat>0){ 
      if(line[iline] == pat[ipat-1]){ 
      pos := pos + 1; 
      } 
     } 
     ipat:=0; 
     pos := -1; 
     } 
     if(ipat==p) { 
      return; 
     } 
     iline := iline + 1; 
    } 
    return; 
} 

    method delete(line:array<char>, l:nat, at:nat, p:nat) 
    requires line!=null 
    requires l <= line.Length 
    requires at+p <= l 
    modifies line 
    ensures line[..at] == old(line[..at]) 
    ensures line[at..l-p] == old(line[at+p..l]) 
{ 
    var i:nat := 0; 
    while(i < l-(at+p)) 
    invariant i <= l-(at+p) 
    invariant at+p+i >= at+i 
    invariant line[..at] == old(line[..at]) 
    invariant line[at..at+i] == old(line[at+p..at+p+i]) 
    invariant line[at+i..l] == old(line[at+i..l]) // future is untouched 
    { 
    line[at+i] := line[at+p+i]; 
    i := i+1; 
    } 
} 

Answer 1

Это довольно трудная вещь, чтобы доказать. Вот некоторые первоначальные идеи, которые могут вам помочь.

Вам необходимо найти меру прерывания для цикла. Я бы предложил использовать что-то вроде кортежа из числа вхождений шаблона и длины строки.

Вы должны быть очень осторожны, чтобы замена не содержала поисковый запрос, иначе ваш цикл может не завершиться. И даже если это прекратится, трудно найти меру завершения, которая будет уменьшаться на каждой итерации.

Например, я хочу заменить «fggf» на «gg» в строке «ffggff», в первый раз по циклу у меня будет 1 появление «fggf» и замена «fggf» на «gg «приводит к« fggf »- поэтому у меня все еще есть одно событие! Во второй раз я закончил с «gg».

Вам нужно будет что-то вроде функции:

function occurences(line:array<char>, l:int, pat:array<char>, p:int) : int 
    reads line 
    requires line != null 
    requires pat != null 
    requires 0 <= l < line.Length 
    requires 0 <= p < pat.Length 

И затем использовать его в петле, как

ghost var matches := occurrences(line, l, dst, n); 

    while(at != -1) 
     decreases matches 
     invariant -1<=at<=l 
     invariant matches == occurrences(line, l, dst, n) 
    { 
     at := find(line, l, dst, n); 
     delete(line, l, at, p); 
     insert(line, l, pat, p, at); 
     matches := matches - 1; 
    } 

Но, как я уже говорил, количество вхождений само по себе не достаточно, чтобы доказать завершение. Вы можете использовать любой расчет в качестве меры завершения. Пока он уменьшается в каждой итерации цикла и не имеет бесконечных нисходящих цепей.