Dafny violation de l'assertion récursive

Question

Je suis nouveau à dafny et j'essaie d'obtenir ce simple morceau de code au travail. Je veux compter les occurrences d'un caractère dans une chaîne. Je reçois une violation d'assertion à la ligne 4. Je sais que ma fonction est de trouver la bonne quantité de caractères, mais il y a clairement quelques failles dans cette assertion. J'essaie d'obtenir les bases avant que je commence à utiliser les conditions pré et post et quoi que ce soit, et cela devrait être possible sans eux. La fonction vérifie simplement le dernier caractère de la chaîne et renvoie un 1 ou un 0, en appelant à nouveau la fonction qui coupe la queue de la chaîne jusqu'à ce qu'elle soit vide.

method Main() { 
    var s:string := "hello world"; 
    print tally(s, 'l'); 
    assert tally(s,'l') == 3; 
} 
function method tally(s: string, letter: char): nat 
{ 
    if |s| == 0 then 0 
    else if s[|s|-1] == letter then 1+tally(s[..|s|-1], letter) 
    else 0 + tally(s[..|s|-1], letter) 
} 

http://rise4fun.com/Dafny/2lvt Voici le lien vers mon code.

Answer 1

Il est naturel de penser que le vérificateur statique Dafny peut évaluer n'importe quel code, comme l'expression dans votre déclaration assert. Le vérificateur essaie d'évaluer des expressions comme celles-ci où les arguments sont donnés comme des constantes (comme votre "hello world", 'l', et 3). Cependant, le vérificateur statique veut éviter de récurer pour toujours (ou même récursif pendant trop longtemps), donc il ne traverse pas toujours complètement ces expressions. Dans votre cas, il y a aussi des limites à ce que le vérificateur est capable de faire avec les opérations de séquence. Donc, en court, bien que le vérificateur essaie d'être utile, il n'est pas toujours arriver au bas des récursions.

Vous pouvez contourner ces limites de deux manières pour que le vérificateur accepte votre assertion.

La manière la plus fiable de déboguer la situation est de commencer par des entrées plus petites et de constituer les entrées les plus longues que vous utilisez. Ceci est assez fastidieux, cependant, et il vous fait apprécier quand Dafny est capable de faire ces choses automatiquement. Ce qui suit (qui vérifie) illustre ce que vous feriez:

var s := "hello world"; 
assert tally("he",'l') == 0; 
assert tally("hel",'l') == 1; 
assert "hell"[..3] == "hel"; 
assert tally("hell",'l') == 2; 
assert "hello"[..4] == "hell"; 
assert tally("hello",'l') == 2; 
assert "hello "[..5] == "hello"; 
assert tally("hello ",'l') == 2; 
assert "hello w"[..6] == "hello "; 
assert tally("hello w",'l') == 2; 
assert "hello wo"[..7] == "hello w"; 
assert tally("hello wo",'l') == 2; 
assert "hello wor"[..8] == "hello wo"; 
assert tally("hello wor",'l') == 2; 
assert "hello worl"[..9] == "hello wor"; 
assert tally("hello worl",'l') == 3; 
assert s[..10] == "hello worl"; 
assert tally(s,'l') == 3; 

En fait, la chose que le vérificateur Dafny ne se développe pas (trop fois) pour vous les opérations « prendre » (qui est, les expressions de la forme s[..E]). Les assertions intermédiaires suivantes se vérifieront elles-mêmes et aideront à vérifier l'assertion finale. Ces affirmations intermédiaires montrent ce que le vérificateur ne pense pas faire automatiquement pour vous.

var s := "hello world"; 
assert "he"[..1] == "h"; 
assert "hel"[..2] == "he"; 
assert "hell"[..3] == "hel"; 
assert "hello"[..4] == "hell"; 
assert "hello "[..5] == "hello"; 
assert "hello w"[..6] == "hello "; 
assert "hello wo"[..7] == "hello w"; 
assert "hello wor"[..8] == "hello wo"; 
assert "hello worl"[..9] == "hello wor"; 
assert s[..10] == "hello worl"; 
assert tally(s,'l') == 3; 

Vous pourriez vous demander, "comment diable aurais-je trouvé cela?". Le façon la plus systématique serait de commencer comme dans mon premier exemple ci-dessus. Ensuite, vous pouvez essayer d'élaguer les nombreuses assertions pour voir ce que le vérificateur a besoin de .

(je suis en train de penser que peut-être le vérificateur Dafny pourrait être amélioré pour faire ces opérations, aussi. Il peut causer des problèmes de performance ailleurs. Je prendrai un coup d'oeil.)

L'autre façon de travailler autour des limites du vérificateur est de définir la fonction tally d'une manière différente, en évitant notamment les opérations "take" , que le vérificateur ne veut pas développer beaucoup.Il est pas clair quoi changer pour rendre le vérificateur heureux dans ces situations, ou si c'est même possible du tout, donc cette solution de contournement peut ne pas être le meilleur. Néanmoins, j'ai essayé la définition suivante de tally et rend votre affirmation passer par:

function method tally'(s: string, letter: char): nat 
{ 
    tally_from(s, letter, 0) 
} 
function method tally_from(s: string, letter: char, start: nat): nat 
    requires start <= |s| 
    decreases |s| - start 
{ 
    if start == |s| then 0 
    else (if s[start] == letter then 1 else 0) + tally_from(s, letter, start+1) 
} 

Notez que ces définitions ne pas utiliser toutes les opérations « prendre ». Ici, le vérificateur est heureux de développer tous les appels récursifs jusqu'à ce que la réponse finale soit trouvée.

Rustan