Formellement vérifier l'exactitude d'un algorithme

StackOverflow https://stackoverflow.com/questions/2149562

Question

Tout d'abord, est-ce possible sur des algorithmes qui ont pas d'effets secondaires?

En second lieu, où je pourrais en apprendre davantage sur ce processus, tous les bons livres, articles, etc?

Était-ce utile?

La solution

COQ est un assistant de preuve qui produit la sortie OCaml correcte. Il est assez compliqué cependant. Je ne ai jamais eu le temps de regarder, mais mon collègue de travail a commencé et cessé de l'utiliser au bout de deux mois. Il était surtout parce qu'il voulait faire avancer les choses plus vite, mais si vous avez besoin de vérifier un algorithme cela pourrait être une bonne idée.

Voici un cours qui utilise COQ et parle des algorithmes prouvant.
Et Voici un tutoriel sur la rédaction de documents académiques COQ.

Autres conseils

  1. Il est généralement beaucoup plus facile pour vérifier / prouver la justesse en l'absence d'effets secondaires sont impliqués, mais ce n'est pas une exigence absolue.
  2. Vous pouvez regarder une partie de la documentation pour un langage de spécification formelle comme Z . Une spécification formelle est pas une preuve elle-même, mais elle est souvent la base pour un.

En général, les preuves formelles sont très spécifiques à l'algorithme à portée de main.

Cependant, il y a plusieurs trucs bien connus qui sont utilisés et réutilisés à nouveau. Par exemple, avec des algorithmes récursifs vous pouvez utiliser invariants.

Une autre astuce commune réduit le problème d'origine à un problème qui est plus facile de montrer la preuve de la justesse de votre algorithme, puis soit généralisant le problème plus facile ou montrant que le problème plus facile peut être traduit à une solution au problème d'origine. est une description.

Si vous avez un algorithme particulier à l'esprit, vous pouvez faire mieux demander comment construire une preuve de cet algorithme plutôt qu'une réponse générale.

Acheter ces livres: http://www.amazon.com/Science-Programming -Monographs-Informatique / dp / 0387964800

Le livre Gries, la programmation scientifique est grande substance. Patient, complet, complet.

Je pense que la vérification de l'exactitude d'un algorithme serait de valider sa conformité avec un cahier des charges. Il y a une branche de la science informatique théorique appelé Méthodes formelles qui peut être ce que vous cherchez si vous avez besoin de se rapprocher de la preuve que vous pouvez. De wikipedia,

  

Méthodes formelles sont un type particulier   techniques de base mathématiquement pour   la spécification, le développement et   la vérification des logiciels et du matériel   systèmes

Vous pourrez trouver de nombreuses ressources et outils d'apprentissage de la multitude de liens sur la page de Wikipédia liés et de la Méthodes formelles wiki .

Logique en informatique, par Huth et Ryan, donne un aperçu assez lisible des systèmes modernes pour la vérification des systèmes. Il était une fois les gens ont parlé de prouver des programmes corrects - avec des langages de programmation qui peuvent ou peuvent ne pas avoir des effets secondaires. L'impression que je reçois de ce livre et ailleurs que les applications réelles sont différentes - par exemple prouvant qu'un protocole est correct, ou que l'unité à virgule flottante d'une puce peut diviser correctement, ou qu'une routine sans verrouillage pour manipuler des listes chaînées est correcte.

Informatique ACM Enquêtes Vol 41 Numéro 4 (Octobre 2009) est un numéro spécial sur la vérification du logiciel. Il semble que vous pouvez obtenir au moins un des documents sans un compte ACM en recherchant « Méthodes formelles: la pratique et l'expérience ».

L'outil Frama-C , pour lequel Elazar propose une vidéo de démonstration dans les commentaires, donne vous un langage de spécification, ACSL , pour l'écriture des contrats de fonction et divers analyseurs pour vérifier qu'une fonction C satisfait ses propriétés de contrat et de sécurité tels que l'absence d'erreurs d'exécution.

Un tutoriel étendu, ACSL par exemple , montre des exemples de algorithmes réels C étant spécifiées et vérifiées, et sépare les fonctions sans effet du côté de ceux effectful (ceux-libre d'effets secondaires sont considérés comme plus facile et viennent en premier dans le tutoriel). Ce document est également intéressant en ce sens qu'il n'a pas été écrit par les concepteurs des outils dont elle a décrire, lui donne un look plus frais et plus didactique à ces techniques.

Non affilié à StackOverflow
scroll top