boucle invariantes pas assez fort lors de la manipulation (tableau) champs de cette

Question

MIS À JOUR

problèmes à résoudre certains problèmes de Dafny, décrits ci-dessous avec la classe donnée et les méthodes respectives. Si vous avez besoin d'autre chose, dites-le moi, merci d'avance. Aussi le lien est mis à jour avec tout ce code dans rise4fun.

class TextEdit { 
var text:array<char>; //conteúdo 
var scrap: array<char>; //conteúdo temporariamente guardado para copy/paste 
var tlen:int; //length di text 
var slen:int; //length di scrap 
var at:int; //current position 
var sellen:int; //length of the selection 


method key(ch:char) 
modifies this, text; 
requires TextInv(); 
requires tlen+1<text.Length && sellen == 0; 
ensures TextInv(); 
{ 
    var tempChar:array<char> := new array<char>; 
    tempChar[0] := ch; 

    insert(text, tlen, tempChar, 1, at); 
    at := at + 1; 
    tlen := tlen + 1; 
} 


method select(sel:int, sl:int) 
modifies this; 
requires TextInv() && 0 <= sel && 0 <= sl && 0 <= sel+sl <= tlen; 
ensures TextInv(); 
{ 
    at := sel; 
    sellen := sl; 
} 

method copy() 
modifies this,scrap; 
requires TextInv() && sellen > 0; 
requires scrap != null; 
ensures TextInv(); 
ensures slen == sellen; 
{ 

    //emptying scrap 
    delete(scrap, slen, 0, slen); 
    slen := 0; 

    var i:int := 0; 
    while(i<sellen) 
    invariant 0<=i<=sellen; 
    invariant slen == i; 
    //cada posição do scrap estará vazia 
    //invariant forall j :: 0<=j<i ==> scrap[j] == ' '; 
    //só depois será preenchida 
    invariant forall k :: i<=k<sellen ==> scrap[k] == text[at+k]; 
    { 
    scrap[i] := text[at+i]; 
    slen := slen + 1; 
    i := i + 1; 
    } 

} 

method cut() 
requires scrap!=null && text!=null; 
modifies this,text, scrap; 
requires TextInv() && sellen > 0; 
ensures TextInv(); 
ensures slen == sellen; 
{ 
    //emptying scrap 
    delete(scrap, slen, 0, slen); 
    slen := 0; 

    var i:int := 0; 
    while(i<sellen) 
    invariant i<=0<=sellen; 
    //cada posição do scrap estará vazia 
// invariant forall j :: 0<=j<i ==> scrap[j] == ' '; 
    //só depois será preenchida 
    invariant forall k :: i<=k<sellen ==> scrap[k] == text[at+k]; 
    { 
    scrap[i] := text[at+i]; 
    slen := slen + 1; 
    i := i + 1; 
    } 
    delete(text, tlen, at, sellen); 

    tlen := tlen - slen; 
    } 


method paste() 
modifies this,text; 
requires TextInv() && 0 <= slen+tlen < text.Length && sellen == 0; 
ensures TextInv(); 
ensures tlen == old(tlen)+slen; 
ensures at == old(at)+slen; 
{ 
    if(slen>0) 
    { 
    insert(text, tlen, scrap, slen, at); 
    tlen := tlen + slen; 
    at := at + slen; 
    } 
} 

function TextInv():bool 
reads this; 
{ 
text != null && 0 <= tlen <= text.Length && scrap != text && 
0 <= at <= tlen && 0 <= sellen && 0 <= at+sellen <= tlen && 
scrap != null && 0 <= slen <= scrap.Length == text.Length 
} 
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 line != null; 
    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 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!=null 
    ensures line[..at] == old(line[..at]) 
    ensures line[at..l-p] == old(line[at+p..l]) 
    ensures forall i :: l-p <= i < l ==> line[i] == ' ' 
{ 
    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; 
    } 

    var j:nat := l-p; 
    while(j < l) 
    invariant l-p <= j <= l 
    invariant line[..at] == old(line[..at]) 
    invariant line[at..l-p] == old(line[at+p..l]) 
    invariant forall i :: l-p <= i < j ==> line[i] == ' ' 
    { 
    line[j] := ' '; 
    j := j+1; 
    } 
} 
} 

On rise4fun

Answer 1

je l'ai trouvé du mal à comprendre ce que votre code est censé faire - la plupart du temps parce que les noms de variables sont difficiles à comprendre. Je l'ai donc fait vérifier en renforçant aveuglément les invariants jusqu'à ce qu'il soit passé. Dans un cas, cut, j'ai dû ajouter une précondition supplémentaire à la méthode. Je ne sais pas si cela est approprié à votre situation ou non, mais je pense que cela reflète la réalité de la méthode (telle qu'elle est).

Vous devez donner le tableau d'une taille lorsque vous allouez il:

var tempChar:array<char> := new char[1]; 

Vous devez ajouter « not null » faits dans votre boucle invariants:

invariant scrap != null && text != null; 

Vous devez ajouter suffisamment faits pour établir que les accès de tableau sont dans les limites, par exemple:

invariant sellen <= scrap.Length 
invariant at+sellen <= text.Length 
invariant 0 <= at 

I fortement vous recommandons d'utiliser des tranches plutôt que la quantification forall k. Il est difficile d'obtenir une telle quantification forall correcte, il est plus difficile à lire, et est souvent moins utile pour le vérificateur:

invariant scrap[..i] == text[at..at+i]; 

L'objet this est dans le jeu de votre modifie la boucle. Vous avez donc besoin de dire que votre boucle n'a pas gâcher ses champs:

modifies this,scrap 
invariant TextInv() 

Vous devez dire que l'objet dans le tableau scrap est toujours le même que celui qui est dans les modifie ensemble de la méthode:

invariant scrap == old(scrap) 

Autres notes:

1. considier à l'aide nat au lieu de int si vous n'avez pas besoin d'une variable d'avoir des valeurs négatives
2. vous pouvez souvent le faire vérifier en partant de la postcondition et en reculant. Continuez simplement à renforcer les invariants et les conditions préalables jusqu'à ce que cela fonctionne. Bien sûr, vous pouvez découvrir que les conditions préalables sont maintenant trop fortes - si c'est le cas, vous avez besoin d'une implémentation plus performante.

http://rise4fun.com/Dafny/GouxO

class TextEdit { 
var text:array<char>; //conteúdo 
var scrap: array<char>; //conteúdo temporariamente guardado para copy/paste 
var tlen:int; //length di text 
var slen:int; //length di scrap 
var at:int; //current position 
var sellen:int; //length of the selection 


method key(ch:char) 
modifies this, text; 
requires TextInv(); 
requires tlen+1<text.Length && sellen == 0; 
ensures TextInv(); 
{ 
    var tempChar:array<char> := new char[1]; 
    tempChar[0] := ch; 

    insert(text, tlen, tempChar, 1, at); 
    at := at + 1; 
    tlen := tlen + 1; 
} 


method select(sel:int, sl:int) 
modifies this; 
requires TextInv() && 0 <= sel && 0 <= sl && 0 <= sel+sl <= tlen; 
ensures TextInv(); 
{ 
    at := sel; 
    sellen := sl; 
} 

method copy() 
modifies this,scrap; 
requires TextInv() && sellen > 0; 
requires scrap != null; 
ensures TextInv(); 
ensures slen == sellen; 
{ 
    //emptying scrap 
    delete(scrap, slen, 0, slen); 
    slen := 0; 

    var i:nat := 0; 
    while(i<sellen) 
    modifies this,scrap 
    invariant TextInv() 
    invariant 0<=i<=sellen; 
    invariant slen == i; 
    //cada posição do scrap estará vazia 
    //invariant forall j :: 0<=j<i ==> scrap[j] == ' '; 
    //só depois será preenchida 
    invariant scrap != null && text != null; 
    invariant sellen <= scrap.Length 
    invariant at+sellen <= text.Length 
    invariant 0 <= at 
    invariant scrap[0..i] == text[at..at+i]; 
    invariant scrap == old(scrap) 
    { 
    scrap[i] := text[at+i]; 
    slen := slen + 1; 
    i := i + 1; 
    } 
} 

method cut() 
//requires scrap!=null && text!=null; 
modifies this,text, scrap; 
requires TextInv() && sellen > 0; 
requires 0 <= at+sellen <= (tlen - (slen + sellen)); 
ensures TextInv(); 
ensures slen == sellen; 
{ 
    //emptying scrap 
    delete(scrap, slen, 0, slen); 
    slen := 0; 

    assert 0 <= at+sellen <= (tlen - (slen + sellen)); 

    var i:int := 0; 
    while(i<sellen) 
    invariant 0<=i<=sellen; 
    //cada posição do scrap estará vazia 
    //invariant forall j :: 0<=j<i ==> scrap[j] == ' '; 
    //só depois será preenchida 
    invariant scrap != null && text != null; 
    invariant i <= scrap.Length 
    invariant 0 <= at 
    invariant at+i <= text.Length 
    invariant scrap[0..i] == text[at..at+i]; 
    invariant slen + (sellen-i) <= scrap.Length; 
    invariant slen + (sellen-i) == sellen; 
    invariant TextInv() 
    invariant scrap == old(scrap) 
    invariant text == old(text) 
    invariant 0 <= at+sellen <= (tlen - (slen + (sellen-i))); 
    { 
    scrap[i] := text[at+i]; 
    slen := slen + 1; 
    i := i + 1; 

    /*assert text != null; 
    assert 0 <= tlen <= text.Length ; 
    assert scrap != text ; 
    assert 0 <= at <= tlen ; 
    assert 0 <= sellen ; 
    assert 0 <= at+sellen <= tlen ; 
    assert scrap != null ; 
    assert 0 <= slen <= scrap.Length == text.Length;*/ 
    } 

    assert 0 <= at+sellen <= (tlen - slen); 

    delete(text, tlen, at, sellen); 

    assert 0 <= at+sellen <= (tlen - slen); 

    tlen := tlen - slen; 

    assert 0 <= at+sellen <= tlen ; 
} 


method paste() 
modifies this,text; 
requires TextInv() && 0 <= slen+tlen < text.Length && sellen == 0; 
ensures TextInv(); 
ensures tlen == old(tlen)+slen; 
ensures at == old(at)+slen; 
{ 
    if(slen>0) 
    { 
    insert(text, tlen, scrap, slen, at); 
    tlen := tlen + slen; 
    at := at + slen; 
    } 
} 

function TextInv():bool 
reads this; 
{ 
text != null && 0 <= tlen <= text.Length && scrap != text && 
0 <= at <= tlen && 0 <= sellen && 0 <= at+sellen <= tlen && 
scrap != null && 0 <= slen <= scrap.Length == text.Length 
} 
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 line != null; 
    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 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!=null 
    ensures line[..at] == old(line[..at]) 
    ensures line[at..l-p] == old(line[at+p..l]) 
    ensures forall i :: l-p <= i < l ==> line[i] == ' ' 
{ 
    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; 
    } 

    var j:nat := l-p; 
    while(j < l) 
    invariant l-p <= j <= l 
    invariant line[..at] == old(line[..at]) 
    invariant line[at..l-p] == old(line[at+p..l]) 
    invariant forall i :: l-p <= i < j ==> line[i] == ' ' 
    { 
    line[j] := ' '; 
    j := j+1; 
    } 
} 
}