Je travaille sur l'utilisation de dafny pour vérifier un tri d'insertion en utilisant des éléments adjacents "swap" mais je ne trouve pas d'invariant raisonnable pour la boucle while, quelqu'un peut-il m'aider? Voici le lien: http://rise4fun.com/Dafny/wmYMEDafny vérifie le tri d'insertion en utilisant swap
Il y a quelques problèmes ici. D'abord, votre boucle interne n'est pas correcte, car la variable temp n'est jamais mise à jour. Je recommande de supprimer temp et d'utiliser la condition de boucle down >= 0 && a[down+1] < a[down] à la place. Deuxièmement, vous avez plusieurs problèmes avec l'invariant de la boucle interne qui est mal formé (index hors plage, violation de la condition préalable sorted). Cependant, au lieu de les corriger, je recommande de jeter les deux invariants de la boucle interne et d'essayer à nouveau.
Mon invariant préféré pour le type de boucle d'insertion interne est "a[0..up+1] est trié sauf éventuellement à down + 1". Vous pouvez l'indiquer comme
invariant forall j,k | 0 <= j < k < up+1 && k != down+1 :: a[j]<=a[k]
Le fichier résultant vérifie.
invariant de problème est dans la ligne 19 –