Tout d'abord, est-ce seulement possible sur des algorithmes qui n'ont pas d'effets secondaires? Deuxièmement, où pourrais-je en apprendre davantage sur ce processus, les bons livres, articles, etc?Vérification formelle de l'exactitude d'un algorithme
COQ est un assistant de preuve qui produit une sortie ocaml correcte. C'est plutôt compliqué. Je n'ai jamais eu le temps de le regarder, mais mon collègue a commencé et a cessé de l'utiliser après deux mois. C'était surtout parce qu'il voulait faire avancer les choses plus rapidement, mais si vous avez besoin de vérifier un algorithme, cela pourrait être une bonne idée.
Here is a course qui utilise COQ et parle d'algorithmes de vérification.
Et here is a tutorial sur la rédaction d'articles universitaires en COQ.
aussi, ici, http://www.lix.polytechnique.fr/coq/getting-started – nlucaroni
Habituellement, les preuves d'exactitude sont très spécifiques à l'algorithme en question.
Cependant, il existe plusieurs astuces bien connues qui sont utilisées et réutilisées. Par exemple, avec des algorithmes récursifs, vous pouvez utiliser loop invariants. Une autre astuce courante consiste à réduire le problème d'origine à un problème pour lequel la preuve d'exactitude de votre algorithme est plus facile à montrer, puis à généraliser le problème plus facile ou à montrer que le problème le plus simple peut être résolu. Here est une description.
Si vous avez un algorithme particulier en tête, vous pouvez faire mieux en demandant comment construire une preuve pour cet algorithme plutôt qu'une réponse générale.
Réduction de l'algorithme (en particulier décrit dans le lien que vous proposez) est un outil théorique pour démontrer qu'un problème est au moins aussi difficile qu'un autre. Ces preuves, souvent faites dans le modèle de calcul de la machine de Turing, sont des ondulations de la main et rien de comparable à des preuves formelles (vérifiables par machine). Ils sont souvent faits pour que les problèmes soient difficiles à utiliser dans la pratique (l'exemple dans votre lien est pour le problème d'arrêt, montrer qu'un problème est NP-difficile en réduisant un problème NP-difficile connu est également populaire). En bref, je ne suis pas sûr que la réduction des problèmes, comme liée, a quelque chose à voir avec la correction formelle. –
Hmm peut-être la réduction n'est pas le terme correct que je devrais utiliser ici. Quand je dis réduction, je voulais dire quelque chose dans le sens de l'exemple suivant. Supposons que vous ayez un algorithme qui calcule l'intersection de N rectangles, ce que vous savez est correct. Supposons que vous ayez un autre problème pour lequel il existe une traduction non triviale de ce problème au problème de calcul de l'intersection de N rectangles. Ensuite, vous utilisez le premier algorithme pour calculer la solution à ce dernier problème.Tout ce qui reste montre que la traduction est correcte. – ldog
Mais je peux voir que cela est déroutant, c'est une astuce qui repose sur le fait que vous utilisez un algorithme connu qui est connu pour être correct (dans ce cas, celui de calculer l'intersection de N rectangles.) Je peux voir où la confusion vient à savoir s'il s'agit d'une méthode de prouver ou de fournir un algorithme correct. – ldog
Je pense que la vérification de l'exactitude d'un algorithme validerait sa conformité à une spécification. Il ya une branche de l'informatique théorique appelée Formal Methods qui peut être ce que vous cherchez si vous avez besoin de vous rapprocher le plus possible de la preuve. De wikipedia,
Méthodes formelles sont un type particulier des techniques basées mathématiquement pour la spécification, le développement et vérification des logiciels et du matériel systèmes
Vous pourrez trouver beaucoup d'apprentissage ressources et outils de la multitude de liens sur la page Wikipedia liée et de la Formal Methods wiki.
Acheter ces livres: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Le livre Gries, la programmation scientifique est grande substance. Patient, complet, complet.
Et si vous aimez Z, soyez sûr que vous trouverez des outils pour l'incorporer dans le processus d'écriture d'un algorithme formellement correct: http : //www.bmethod.com/php/methode-b-en.php –
Logique en informatique, par Huth et Ryan, donne un aperçu raisonnablement lisible des systèmes modernes pour la vérification des systèmes.Il était une fois les gens ont parlé de prouver les programmes corrects - avec des langages de programmation qui peuvent avoir ou non des effets secondaires. L'impression que je reçois de ce livre et d'ailleurs est que les applications réelles sont différentes - par exemple prouver qu'un protocole est correct, ou que l'unité à virgule flottante d'une puce peut se diviser correctement ou qu'une routine sans verrou pour manipuler des listes liées est correcte. ACM Computing Surveys Vol 41 Numéro 4 (Octobre 2009) est un numéro spécial sur la vérification de logiciels. Il semble que vous puissiez accéder à au moins un des documents sans compte ACM en recherchant «Méthodes formelles: pratique et expérience».
Les "méthodes formelles" englobent tous les objectifs que vous avez cités. Je suis dans le sous-domaine des «programmes corrects» et je dois admettre que jusqu'à présent les grands succès industriels sont venus des autres sous-domaines (attendez jusqu'à l'année prochaine!). Une conférence comme celle de FMWEEK est quelque peu déroutante car elle rassemble des gens avec toutes ces différentes approches et objectifs, mais nous avons beaucoup en commun et beaucoup à échanger. –
L'outil Frama-C, pour lequel Elazar propose une vidéo de démonstration dans les commentaires, vous donne un langage de spécification, ACSL, pour les contrats de fonction d'écriture et différents analyseurs permettant de 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 by example, montre des exemples d'algorithmes C réels spécifiés et vérifiés, et sépare les fonctions sans effets secondaires des effets efficaces (les effets sans effets secondaires sont considérés plus faciles et viennent en premier dans le Didacticiel). Ce document est également intéressant en ce qu'il n'a pas été écrit par les concepteurs des outils qu'il décrit, il donne donc un regard plus frais et plus didactique sur ces techniques.
Si vous êtes familier avec LISP alors vous devriez certainement vérifier ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
Dijkstra de Discipline de la programmation et ses EWDS jeter les bases d'une vérification formelle en tant que science dans la programmation. Un travail plus simple est la programmation systématique de Wirth, qui commence par l'approche simple de l'utilisation de la vérification. Wirth utilise pré-ISO Pascal pour la langue; Dijkstra utilise un formalisme semblable à Algol-68 appelé Guarded (GCL). La vérification formelle a mûri depuis Dijkstra et Hoare, mais ces textes plus anciens peuvent encore être un bon point de départ.
L'outil PVS développé par Stanford guys est un système de spécification et de vérification. J'ai travaillé dessus et je l'ai trouvé très utile pour Theoram Proving.
WRT (1), vous devrez probablement créer un modèle de l'algorithme d'une manière qui "capture" les effets secondaires de l'algorithme dans une variable de programme destinée à modéliser de tels effets secondaires basés sur l'état.
Je ne suis pas sûr de savoir ce que vous voulez dire au sujet des effets secondaires. – ldog
Voir ceci: http://en.wikipedia.org/wiki/Side_effect_%28computer_science%29 – joemoe
Voir http://stackoverflow.com/questions/476959/why-cant-programs-be-proven qui a quelques bonnes réponses. –