Dafny méthode d'insertion, une postcondition ne peut pas tenir sur ce chemin de retour

Question

J'ai un tableau "ligne" qui contient une chaîne de longueur "l" et un tableau "nl" qui contient une chaîne de longueur "p". Note: "l" et "p" ne doivent pas nécessairement être la longueur de chaque tableau correspondant. Le paramètre "at" sera la position où l'insertion sera faite dans "line". Reprise: Un tableau de longueur "p" sera inséré dans "ligne", en déplaçant tous les caractères de "ligne" entre la position (at, i, at + p), 'p' positions vers la droite afin de rendre l'insertion .

Ma logique pour les garanties est de vérifier si les éléments insérés en "ligne" ont le même ordre et sont les mêmes que les caractères contenus dans "nl".

Voici the code:

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 && 0 <= p <= nl.Length ; 
    requires 0 <= at <= l; 
    modifies line; 
    ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i]; // error 
{ 
    var i:int := 0; 
    var positionAt:int := at; 
    while(i<l && positionAt < l) 
    invariant 0<=i<l+1; 
    invariant at<=positionAt<=l; 
    { 
    line[positionAt+p] := line[positionAt]; 
    line[positionAt] := ' '; 
    positionAt := positionAt + 1; 
    i := i + 1; 
    } 

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

Voici les errors que je reçois.

Merci.

Answer 1

Je soupçonne que votre algorithme est incorrect, car il ne semble pas tenir compte du fait que le décalage des caractères à partir de la position at par endroits p pourrait les écrire sur la fin de la chaîne dans line.

Mon expérience a été que pour réussir avec la vérification

1. bonnes normes de développement de code sont cruciales. Une bonne dénomination de variable, formatage de code, et d'autres conventions de code sont encore plus important que d'habitude.
2. L'écriture de code logiquement simple est vraiment utile. Essayez d'éviter les variables supplémentaires inutiles. Essayez de simplifier les expressions arithmétiques et logiques dans la mesure du possible.
3. Démarrer avec un algorithme correct facilite la vérification. Bien sûr, c'est plus facile à dire qu'à faire!
4. Il est souvent utile d'écrire les invariants de boucle les plus forts auxquels vous pouvez penser.
5. Travailler en arrière à partir de la postcondition est souvent utile. Dans votre cas, prenez la postcondition et la négation de la condition de boucle finale - et utilisez-les pour déterminer ce que doit être l'invariant de la boucle finale pour impliquer la postcondition. Reculez ensuite de la boucle précédente, etc.
6. Lors de la manipulation de tableaux, l'utilisation d'une variable fantôme contenant la valeur originale du tableau en tant que séquence est très souvent une stratégie efficace. Les variables Ghost n'apparaissent pas dans la sortie du compilateur, cela n'affectera pas les performances de votre programme.
7. Il est souvent utile d'écrire des assertions pour l'état exact du tableau, même si la postcondition ne nécessite qu'une propriété plus faible.

Voici une application contrôlée de votre procédure souhaitée:

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

http://rise4fun.com/Dafny/ZoCv