Schleifeninvariante nicht stark genug, um bei der Manipulation (Array) Felder dieser

Question

UPDATED

Probleme auf einigen dafny Probleme zu lösen, mit der gegebenen Klasse und jeweiligen Verfahren beschrieben. Wenn Sie etwas anderes brauchen, bitte sagen Sie mir, ich danke Ihnen im Voraus. Auch der Link wird mit diesem Code in Rise4fun aktualisiert.

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

Ich fand es schwer zu verstehen, was Ihr Code tun soll - vor allem, weil die Variablen Namen schwer zu verstehen sind. Also habe ich es gerade erst verifiziert, indem ich die Invarianten blind gestärkt habe, bis es vorbei ist. In einem Fall, , musste ich eine zusätzliche Bedingung zu der Methode hinzufügen. Ich weiß nicht, ob das für Ihre Situation angemessen ist oder nicht, aber ich denke, es spiegelt wider, was die Methode (so wie sie ist) tatsächlich erfordert.

Sie benötigen das Array eine Größe geben, wenn Sie es zuweisen:

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

Sie müssen „nicht null“ Fakten in Ihre Schleifeninvarianten hinzuzufügen:

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

Sie müssen ausreichend hinzufügen Tatsachen festzustellen, dass die Array-Zugriffe in Grenzen sind, wie zB:

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

I stark empfehlen, dass Sie Scheiben anstelle der forall k Quantifizierung verwenden. Es ist schwierig, solche forall Quantifizierung korrekt zu erhalten, ist es schwieriger, zu lesen, und ist oft weniger nützlich für den Verifizierer:

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

Das this Objekt in dem modifizierende Ihrer Schleife gesetzt. Sie müssen also sagen, dass Ihre Schleife nicht Chaos tat bis seine Felder:

modifies this,scrap 
invariant TextInv() 

Sie müssen sagen, dass das Objekt in dem scrap Array ist immer noch das gleiche, die in dem modifizierende gesetzt des Verfahrens:

invariant scrap == old(scrap) 

Andere Anmerkungen:

1. considier nat statt int verwenden, wenn Sie negative Werte eine Variable nicht brauchen, um
2. Sie können es oft überprüfen, indem Sie von der Nachbedingung beginnen und rückwärts arbeiten. Verstärke einfach die Invarianten und Vorbedingungen, bis es funktioniert. Natürlich können Sie feststellen, dass die Voraussetzungen jetzt zu stark sind - wenn Sie eine leistungsfähigere Implementierung benötigen.

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