Au Software Engineering Stack Exchange, j'ai vu cette question : "Qu'est-ce qui empêche l'adoption généralisée des méthodes formelles?" La question a été fermée car biaisée, et la plupart des réponses étaient des commentaires comme «Trop cher !!!» ou "Un site n'est pas un avion !!!" D'une certaine manière, c'est vrai, mais cela n'explique pas grand-chose. J'ai écrit cet article pour donner une image historique plus large des méthodes formelles (FM), pourquoi elles ne sont pas réellement utilisées et ce que nous faisons pour corriger la situation.

Avant de commencer, vous devez formuler certaines conditions. En fait, il n'y a pas beaucoup de méthodes formelles: seulement quelques petits groupes . Cela signifie que différents groupes utilisent les termes différemment. D'une manière générale, il existe deux groupes de méthodes formelles: la spécification formelle étudie la rédaction de spécifications précises et non ambiguës, et la vérification formelle étudie les méthodes de preuve. Cela inclut à la fois le code et les systèmes abstraits. Non seulement nous utilisons des termes différents pour le code et les systèmes, mais nous utilisons souvent différents outils pour les vérifier. Pour rendre les choses encore plus confuses, si quelqu'un dit qu'il crée une spécification formelle, cela signifie généralement une vérification de la conception. Et si quelqu'un dit qu'il fait une vérification formelle, cela se réfère généralement à la vérification du code.

Pour plus de clarté, nous diviserons la vérification en vérification de code (CV) et vérification de conception (DV) et de la même manière divisons les spécifications en CS et DS. Ces termes ne sont pas couramment utilisés dans la vaste communauté FM. Commençons par CS et CV, puis passons à DS et DV.

De plus, une vérification partielle est possible, où seul un sous-ensemble de la spécification est vérifié, ou une vérification complète . Cela peut être la différence entre les preuves des allégations «le système ne se bloque jamais et n'accepte pas le mauvais mot de passe» ou «le système ne se bloque jamais et ne verrouille pas le compte si vous entrez trois fois le mauvais mot de passe». Fondamentalement, nous supposerons que nous effectuons une vérification complète.

Vous devez également clarifier le type de logiciel que nous formalisons. La plupart des gens identifient implicitement des programmes hautement fiables tels que les appareils médicaux et les avions. Les gens supposent que les méthodes formelles sont largement utilisées pour eux, mais elles ne sont pas nécessaires pour le reste. C'est trop optimiste : la plupart des logiciels très fiables n'utilisent pas de méthodes formelles. Au lieu de cela, nous nous concentrerons sur les logiciels «ordinaires».

Enfin, l'avertissement: je ne suis pas un historien professionnel, et bien que j'aie essayé de vérifier soigneusement les informations, il peut y avoir des erreurs dans l'article. De plus, je me spécialise dans les spécifications formelles (DS et DV), il y a donc plus de risques d'erreur lorsque je parle de vérification de code. Si vous voyez, écrivez-moi, je vais le réparer (et encore une chose: je gagne de l'argent grâce à des séminaires sur TLA + et Alloy, donc je suis très partisan de ces langues; j'essaie d'être aussi objectif que possible, mais vous comprenez: le parti pris est un parti pris).

Programmation formelle

Obtenir des spécifications

Avant de prouver l'exactitude du code, vous devez obtenir la norme de vérité. Cela signifie une certaine spécification de ce que le code doit faire. Nous devons savoir avec certitude que le résultat correspond à la spécification. Il ne suffit pas de dire que la liste est «triée»: nous ne savons pas ce que nous trions, quels critères nous utilisons et même ce que nous entendons par «tri». Au lieu de cela, nous pouvons dire: "La liste des entiers l triée par ordre croissant pour deux indices i et j quelconques, si i < j , alors l[i] <= l[j] ."

Les spécifications du code sont divisées en trois types principaux:

La première consiste à écrire des instructions indépendantes du code. Nous écrivons notre fonction de tri, et dans un fichier séparé nous écrivons le théorème «cela retourne des listes triées». Il s'agit de la plus ancienne forme de spécification, mais Isabelle et ACL2 fonctionnent toujours de cette façon (ML a été inventé spécifiquement pour aider à rédiger de telles spécifications).
Le second implémente des spécifications dans le code sous la forme de pré et postconditions, déclarations et invariants. Vous pouvez ajouter une postcondition à la fonction selon laquelle "la valeur de retour est une liste triée". Les spécifications basées sur les revendications ont été initialement formalisées dans la logique de Hoar . Ils sont apparus pour la première fois dans le langage de programmation Euclid au début des années 1970 (on ne sait pas qui a commencé à les utiliser: Euclid ou SPV , mais pour autant que je sache, Euclid a été présenté au public auparavant). Ce style est également appelé programmation par contrat - la forme de vérification la plus populaire dans l'industrie moderne (ici, les contrats sont utilisés comme spécifications de code).
Enfin, il existe des systèmes de types. Par correspondance Curry - Howard, tout théorème mathématique ou preuve peut être codé comme un type dépendant. Nous allons définir le type de listes triées et déclarer le type [Int] -> Sorted [Int] pour la fonction.

Sur Let's Prove Leftpad, vous pouvez voir à quoi cela ressemble. HOL4 et Isabelle sont de bons exemples des spécifications du «théorème indépendant», SPARK et Dafny sont les spécifications de la «déclaration imbriquée», et Coq et Agda sont le «type dépendant».

Si vous regardez attentivement, ces trois formes de spécification de code sont comparées aux trois principaux domaines de la validation automatique: les tests, les contrats et les types. Ce n'est pas un hasard. La correction est un large éventail, et la vérification formelle est l'un de ses extrêmes. À mesure que la rigueur (et l'effort) de vérification diminue, nous obtenons des vérifications plus simples et plus étroites, qu'il s'agisse de limiter l'espace d'états à l'étude, d'utiliser des types plus faibles ou de vérifier la force au moment de l'exécution. Ensuite, tout moyen de spécification complète se transforme en moyen de spécification partielle, et vice versa: beaucoup considèrent la salle blanche comme une technique de vérification formelle, où une revue de code va bien au-delà des capacités humaines.

Quelles spécifications sont correctes?

La vérification vérifie que le code est conforme à la spécification. La question se pose: comment savoir si nous avons la bonne spécification? Trouver la bonne spécification est l'un des plus gros problèmes des méthodes formelles. C'est également l'une des principales objections à leur encontre. Mais les sceptiques ici ne signifient pas exactement ce que les spécialistes formels ont en tête.

Lorsque des tiers demandent: «Comment obtenir les bonnes spécifications?» Ils pensent généralement à la validation , c'est-à-dire aux spécifications qui ne répondent pas aux exigences du client. Si vous prouvez formellement que votre code trie la liste et que le client veut réellement Uber pour les soupes (tm), vous venez de passer une tonne de temps. Par exemple, seules des itérations rapides et de courtes boucles de rétroaction peuvent confirmer vos besoins.

Il est vrai que la vérification du code ne le valide pas. Mais il y a deux problèmes avec cet argument. La première est que l'étape d'application des méthodes formelles est simplement reportée, mais ne disparaît pas complètement. Après toutes ces itérations rapides, vous avez probablement déjà une idée de ce que veut le client. Et puis vous commencez la vérification du code. Deuxièmement, bien que nous ne sachions pas exactement ce que veut le client, nous pouvons supposer ce qu'il ne veut absolument pas . Par exemple, pour bloquer accidentellement un logiciel. Ils n'ont pas besoin de failles de sécurité. Tout le monde est d'accord avec cela: au final, personne ne dit que vous devez ignorer les tests unitaires pendant les itérations. Assurez-vous au moins que votre système de contrôle de version ne supprime pas les données utilisateur aléatoires (remarque: ne pensez pas que je suis aigri ou quelque chose comme ça).

Le problème de trouver la bonne spécification est plus fondamental: nous ne savons souvent pas quoi y écrire . Nous pensons à nos besoins en termes humains et non mathématiques. Si je dis: «Le programme devrait distinguer les arbres des oiseaux», alors de quoi s'agit-il? Je peux l'expliquer à une personne en montrant un tas de photos d'arbres et d'oiseaux, mais ce ne sont que des exemples concrets, pas une description de l' idée . En fait, pour traduire cela en une spécification formelle, il est nécessaire de formaliser les concepts humains, et c'est un problème sérieux.

Ne vous méprenez pas. Les spécifications pertinentes peuvent être définies ici, et les experts le font tout le temps. Mais la rédaction des spécifications appropriées est une compétence qui doit être développée, ainsi que des compétences en programmation. C'est pourquoi de nombreux succès récents de la vérification de code s'expliquent par une mise en correspondance claire de ce que nous voulons et de ce que nous pouvons exprimer. Par exemple, CompCert est un compilateur C officiellement vérifié. La spécification est: «Evitez les erreurs de compilation».

Mais tout cela n'a rien à voir avec la vérification. Lorsque vous avez une spécification, vous devez toujours prouver que le code la correspond.

Preuve de spécification

Le tout premier outil de vérification de code est la méthode «pensez à pourquoi c'est vrai» à la manière de Dijkstra, qui concerne principalement ALGOL. Par exemple, je peux «prouver» l'exactitude du tri par la méthode d'insertion comme suit:

L'option de base : si vous ajoutez un élément à la liste vide, ce sera le seul élément, il sera donc trié.
Si nous avons une liste triée avec k éléments et ajoutons un élément, alors nous insérons l'élément de sorte qu'il soit après tous les plus petits nombres et avant tous les plus grands nombres. Cela signifie que la liste est toujours triée.
Par induction, le tri par insertion triera la liste entière.

Évidemment, en réalité, la preuve paraîtra plus rigoureuse, mais c'est une idée générale. Dijkstra et d'autres ont utilisé ce style pour prouver l'exactitude de nombreux algorithmes, y compris de nombreuses bases de la concurrence. C’est aussi le style auquel les mots de Knuth sont associés: «Méfiez-vous des erreurs dans ce code; J'ai seulement prouvé que c'était correct, mais je n'ai pas commencé. " Vous pouvez facilement ruiner une preuve mathématique afin que personne ne le remarque. Selon certaines estimations , environ 20% des preuves mathématiques publiées contiennent des erreurs. Peter Guttmann a un excellent essai sur les preuves de la santé d'un programme ridicule, où des tonnes de code "testé" tombent immédiatement si vous les exécutez.

Dans le même temps, nous avons étudié les moyens de prouver automatiquement les théorèmes mathématiques. Le premier programme pour prouver les théorèmes a été publié en 1967 . Au début des années 1970, de tels programmes ont commencé à être utilisés pour tester le code Pascal, et au milieu de la décennie, des langages formels spéciaux sont apparus. Le programmeur formule certaines propriétés du code, puis crée une preuve vérifiable que le code possède ces propriétés. Les premiers programmes de démonstration de théorèmes ont simplement aidé les gens à vérifier les preuves, tandis que des outils plus sophistiqués pouvaient prouver indépendamment des parties du théorème.

Ce qui conduit au problème suivant.

Les preuves sont difficiles à obtenir

Les preuves sont difficiles et c'est un travail très méchant. Il est difficile de quitter la programmation et d'aller au cirque. Étonnamment, les preuves de code formelles sont souvent plus strictes que les preuves écrites par la plupart des mathématiciens! Les mathématiques sont une activité très créative, où la réponse au théorème n'est valable que si vous le montrez. La créativité va mal avec le formalisme et les ordinateurs.

Prenons le même exemple de tri par insertion où nous avons appliqué l'induction. Tout mathématicien comprendra immédiatement ce qu'est l'induction, comment elle fonctionne en général et comment elle fonctionne dans ce cas. Mais dans le programme de démonstration des théorèmes, tout doit être strictement formalisé. Il en va de même pour la preuve par contradiction, la preuve par contreposition, etc. De plus, toutes les hypothèses doivent être formalisées, même celles où la plupart des mathématiciens ne se soucient pas de la preuve. Par exemple, a + (b + c) = (a + b) + c . Le programme de vérification des théorèmes a priori ne sait pas que cela est vrai. Vous devez soit le prouver (dur), soit le déclarer comme vrai selon la loi associative d'addition (dangereux), soit acheter une bibliothèque de théorèmes à quelqu'un qui a déjà pu le prouver (cher). Les premiers programmes de démonstration de théorèmes rivalisaient dans le nombre de tactiques de preuve intégrées et de bibliothèques de théorèmes connexes. L'un des premiers programmes SPADE répandus a présenté la bibliothèque arithmétique complète comme le principal avantage.

Ensuite, vous devez obtenir la preuve elle-même. Vous pouvez le confier au programme ou l'écrire vous-même. Habituellement, la définition automatique de la preuve n'est pas décidable. Pour les cas extrêmement étroits, tels que la logique propositionnelle ou la vérification de type HM, il est «uniquement» NP-complet. En fait, nous écrivons nous-mêmes la plupart des preuves et l'ordinateur vérifie leur exactitude. Cela signifie que vous devez bien connaître:

mathématiques
l'informatique;
la zone dans laquelle vous travaillez: compilateurs, matériel, etc.;
les nuances de votre programme et de votre spécialisation;
les nuances du programme pour prouver les théorèmes que vous utilisez, ce qui en soi est toute une spécialité.

Pire, des bâtons spécifiques à l'ordinateur sont placés dans des roues. Rappelez-vous, j'ai dit qu'il était dangereux de supposer une loi associative d'addition? Certaines langues ne le respectent pas. Par exemple, en C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 est INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) , qui est indétectable. En supposant un ajout associatif en C ++, votre preuve sera incorrecte et le code sera rompu. Vous devez soit éviter cette déclaration, soit prouver qu'aucun débordement ne se produira jamais pour votre fragment particulier.

Vous pouvez dire que l'addition indéfinie est une erreur, mais vous devez utiliser un langage avec des entiers indépendants. Mais la plupart des langues ont des caractéristiques spécifiques qui interfèrent avec les preuves. Prenez le code suivant:

 a = true; b = false; f(a); assert a;

Est-ce toujours le cas? Pas un fait. Peut-être que f changera a . Peut-être que cela changera le flux parallèle. Peut-être que b attribuer un alias a , donc le changer changera également a (note: les alias rendent si difficile d'écrire des preuves que John C. Reynolds a dû créer une toute nouvelle logique de séparation pour résoudre ce problème). Si quelque chose comme cela est possible dans votre langue, vous devez clairement prouver que cela ne se produit pas ici. Le code propre aidera ici, dans un autre cas, il peut détruire la preuve, car il vous oblige à utiliser la récursivité et les fonctions d'un ordre supérieur. Soit dit en passant, les deux sont la base pour écrire de bons programmes fonctionnels. Ce qui est bon pour la programmation est mauvais pour la preuve! (Remarque: dans cette conférence, Edmund Clark a énuméré certaines des propriétés qui sont difficiles à vérifier: «virgules flottantes, chaînes, types définis par l'utilisateur, procédures, simultanéité, modèles universels, stockage, bibliothèques ...»).

Les vérificateurs formels ont un dilemme: plus le langage est expressif, plus il est difficile de prouver quelque chose. Mais moins la langue est expressive, plus il est difficile d'écrire dessus. Les premiers langages formels de travail étaient des sous-ensembles très limités de langages plus expressifs: ACL2 était un sous-ensemble de Lisp, Euclid était un sous-ensemble de Pascal, etc. Et rien de ce que nous avons discuté jusqu'à présent ne prouve en fait de vrais programmes, ce ne sont que des tentatives d'approche à la rédaction de preuves.

La preuve est difficile. Mais ça devient plus facile. Les chercheurs dans ce domaine ajoutent de nouvelles heuristiques, des bibliothèques de théorèmes, des composants pré-testés, etc. Le progrès technique aide également: plus les ordinateurs sont rapides, plus la recherche est rapide.

Révolution SMT

L'une des innovations du milieu des années 2000 a été l'inclusion de solveurs SMT dans les programmes de démonstration des théorèmes. De manière générale, un solveur SMT peut transformer (certains) théorèmes mathématiques en problèmes de conformité aux contraintes. Cela transforme une tâche créative en une tâche informatique. Vous devrez peut-être encore lui fournir des problèmes intermédiaires (lemmes) comme étapes du théorème, mais c'est mieux que de tout prouver vous-même. Les premiers solveurs SMT sont apparus vers 2004, d'abord comme projets académiques. Quelques années plus tard, Microsoft Research a publié le Z3, un solveur SMT complet. Le gros avantage du Z3 était qu'il devenait beaucoup plus pratique à utiliser que les autres SMT, qui, franchement, ne disaient presque rien. Microsoft Research l'a utilisé en interne pour aider à prouver les propriétés du noyau Windows, donc elles n'étaient pas limitées à une UX minimale.

SMT a frappé la communauté FM à bout de souffle car elle a soudainement rendu triviales de nombreuses preuves simples et lui a permis d'aborder des problèmes très complexes. Ainsi, les gens pouvaient travailler dans des langues plus expressives, car maintenant les problèmes des déclarations expressives commençaient à être résolus. Des progrès incroyables sont évidents dans le projet IronFleet : en utilisant les meilleurs solveurs SMT et un langage de vérification avancé, Microsoft a pu écrire 5 000 lignes de code Dafny éprouvé en seulement 3,7 années-hommes! C'est un rythme incroyablement rapide: jusqu'à quatre lignes entières par jour (note: le précédent record appartenait à seL4 , dont les développeurs écrivaient deux lignes par jour en C.

La preuve est difficile.

Pourquoi est-ce nécessaire?

Il est temps de prendre du recul et de demander: «À quoi ça sert?» Nous essayons de prouver que certains programmes répondent à certaines spécifications. La correction est une plage. La vérification comporte deux parties: le degré de «correction» objective de votre programme et la précision avec laquelle vous avez vérifié l'exactitude. De toute évidence, plus il est vérifié, mieux c'est, mais la vérification vaut le temps et l'argent. Si nous avons plusieurs restrictions (performances, délais de mise sur le marché, coût, etc.), une validation complète n'est pas nécessairement la meilleure option. Ensuite, la question se pose, quel est le contrôle minimum dont nous avons besoin et ce qu'il en coûte. Dans la plupart des cas, par exemple, une exactitude de 90% ou 95% ou 99% vous suffit. Peut-être devriez-vous passer du temps à améliorer l'interface, plutôt que de vérifier les 1% restants?

Puis la question: "Un chèque de 90/95/99% est-il beaucoup moins cher que 100%?" La réponse est oui. Il est assez confortable de dire que la base de code, que nous avons bien testée et typée, est fondamentalement correcte, à l'exception de quelques corrections en production, et nous écrivons même plus de quatre lignes de code par jour. En fait, la grande majorité des dysfonctionnements dans les systèmes distribués auraient pu être évités grâce à des tests légèrement plus complets. Et ce n'est qu'une extension des tests, sans parler du fuzzing, des tests basés sur les propriétés ou des tests de modèles. Vous pouvez obtenir un résultat vraiment exceptionnel avec ces astuces simples sans avoir à obtenir une preuve complète.

Que se passe-t-il si la saisie et les tests ne fournissent pas une vérification suffisante? Il est encore plus facile de passer de 90% à 99% que de 99% à 100%. Comme mentionné précédemment, Cleanroom est une pratique de développeur qui comprend une documentation complète, une analyse approfondie des flux et des révisions de code approfondies. Aucune preuve, aucune vérification formelle, pas même des tests unitaires. Mais une salle blanche correctement organisée réduit la densité des défauts à moins de 1 bogue pour 1000 lignes de code dans la production (note: les chiffres de l'étude Stavley dans Toward Zero-Defect Programming > mais soyez toujours sceptiques et vérifiez la source ). La programmation de Cleanroom ne ralentit pas le rythme de développement, et va certainement plus vite que 4 lignes par jour. Et Cleanroom lui-même n'est qu'une des nombreuses méthodes de développement logiciel hautement fiables qui se situent entre le développement habituel et la vérification du code. Vous n'avez pas besoin d'une vérification complète pour écrire un bon logiciel ou même presque parfait. Il y a des moments où cela est nécessaire, mais pour la plupart des industries, c'est un gaspillage d'argent.

Cependant, cela ne signifie pas que les méthodes formelles ne sont généralement pas économiques. De nombreuses méthodes hautement fiables mentionnées ci-dessus sont basées sur l'écriture de spécifications de code que vous ne prouvez pas officiellement. En termes de vérification, il existe deux façons courantes dont l'industrie bénéficie. Tout d'abord, la vérification de la conception au lieu du code, dont nous discuterons plus tard. Deuxièmement, une vérification partielle du code, que nous allons examiner maintenant.

Vérification partielle du code

Pour les tâches quotidiennes, il est trop coûteux de faire une vérification complète. Que diriez-vous partielle? Après tout, vous pouvez bénéficier de la preuve de certaines propriétés de fragments de code individuels. Au lieu de prouver que ma fonction trie toujours correctement les nombres, je peux au moins prouver qu'elle ne boucle pas indéfiniment et ne sort jamais de la plage. Il s'agit également d'informations très utiles. Ainsi, même les preuves les plus simples pour les programmes C sont un excellent moyen d'éliminer une grande partie des comportements non définis .

Le problème est l' accessibilité .La plupart des langues sont conçues pour une vérification complète ou ne les prennent pas en charge du tout. Dans le premier cas, vous manquez de nombreuses fonctionnalités intéressantes de langages plus expressifs, et dans le second cas, vous avez besoin d'un moyen de prouver les choses dans un langage hostile au concept lui-même. Pour cette raison, la plupart des études sur la vérification partielle se concentrent sur plusieurs langages hautement prioritaires, tels que C et Java. Beaucoup fonctionnent avec des sous-ensembles de langues limités. Par exemple, SPARK est un sous-ensemble limité d'Ada, vous pouvez donc écrire du code SPARK critique et interagir avec du code Ada moins critique. Mais la plupart de ces langues sont assez niches.

Le plus souvent, certains types de vérification sont intégrés dans la structure de base des langues. Les systèmes de typification utilisés dans la production sont une variante courante: vous ne savez peut-être pas que la queue retourne toujours la queue, mais vous savez exactement quel est son type [a] -> [a]. Il existe également des exemples comme Rust avec une sécurité de la mémoire éprouvée et Pony avec une preuve de sécurité avec des exceptions. Ils sont légèrement différents de SPARK et Frama-C en ce qu'ils ne peuvent effectuer que des vérifications partielles. Et ils sont généralement développés par des experts en langages de programmation, et non par des experts en méthodes formelles: il y a beaucoup de points communs entre les deux disciplines, mais ils ne sont pas identiques. C'est peut-être la raison pour laquelle des langues comme Rust et Haskell sont vraiment adaptées à une utilisation pratique.

Spécifications de conception

Jusqu'à présent, nous n'avons parlé que de la vérification du code. Cependant, les méthodes formelles ont un autre côté, qui est plus abstrait et vérifie la conception elle-même, l'architecture du projet. Cette analyse est si profonde qu'elle est synonyme de spécification formelle : si quelqu'un dit qu'il remplit une spécification formelle, cela signifie très probablement qu'il définit et vérifie la conception.

Comme nous l'avons déjà dit, prouver toutes les lignes de code est très, très difficile. Mais de nombreux problèmes de production ne surviennent pas à cause du code, mais à cause de l'interaction des composants du système. Si nous ignorons les détails de la mise en œuvre, par exemple, si nous considérons comme acquis que le système est capable de reconnaître les oiseaux, il nous sera plus facile d'analyser comment les arbres et les oiseaux s'intègrent dans la conception globale en tant que modules de haut niveau. À une telle échelle, il devient beaucoup plus facile de décrire des choses que vous ne pouviez pas réaliser, comme un environnement d'exécution, des interactions humaines ou un flux de temps impitoyable . À cette échelle, nous formalisons nos intentions à l'aide d'un système commun, plutôt que de lignes de code. Ceci est beaucoup plus proche du niveau humain, où les projets et les exigences peuvent être beaucoup plus ambigus qu'au niveau du code.

Par exemple, prenons une procédure avec une spécification approximative «si elle est appelée, elle effectue un appel système pour enregistrer les données dans le référentiel et traite les erreurs système». Les propriétés sont difficiles à vérifier, mais il est assez clair comment procéder. Les données sont-elles sérialisées correctement? Nos garanties sont-elles violées en raison d'une saisie incorrecte? Sommes-nous en train de gérer toutes les manières possibles d'échouer un appel système? Comparez maintenant le système de journalisation de haut niveau avec la spécification «tous les messages sont enregistrés» et répondez aux questions suivantes:

Tous les messages sont-ils enregistrés ou tous les messages qui entrent dans le système ? Les messages sont enregistrés une fois ou garantis une fois?
Comment les messages sont-ils envoyés? Est-ce le tour? La chaîne ne les délivre-t-elle qu'une seule fois? Tout va bien avec la livraison?
? , ? «» , ?
, ? ?
? « » ?
GDPR?
.

Sans une conception formelle, il est plus difficile d'exprimer les exigences vraiment nécessaires pour le système. Si vous ne pouvez pas les exprimer, vous ne savez pas si le design répond vraiment aux exigences ou leur ressemble, mais cela peut entraîner des conséquences imprévisibles. En exprimant plus formellement les intentions et la conception, nous pouvons facilement vérifier que nous développons réellement ce dont nous avons besoin.

Tout comme nous utilisons des langages de programmation pour représenter du code, nous utilisons des langages de spécification pour représenter des projets. Les langages de spécification sont généralement orientés vers les spécifications de conception plutôt que vers les spécifications de code, bien que certains langages puissent être utilisés dans les deux cas (remarque: le processus de mise en correspondance des spécifications de conception avec les spécifications de code est appelé raffinementÀ l'avenir, j'appellerai des langages de conception (DL) pour minimiser la confusion (encore une fois, ce n'est pas une terminologie courante; la plupart des gens utilisent le «langage de spécification», mais je veux faire une distinction claire entre les spécifications de code et les spécifications de conception).

Le premier DL complet était probablement le VDM vers 1972. Depuis lors, nous avons vu une grande variété de langages de spécifications différents. L'espace DL est beaucoup plus diversifié et fragmenté qu'avec les langages de vérification de code (CVL). En gros, les gens ont inventé le DL comme moyen d'atteindre une fin et le CVL comme objectif lui-même. Puisqu'ils sont fortement influencés par des problèmes spécifiques, DL met en œuvre toutes sortes d'idées et de sémantique. Voici un très, très bref aperçu de certaines des premières DL:

La langue	Zone de modélisation	Moyens
Z	exigences commerciales	algèbre relationnelle
Promela		CSP
SDL		-

Étant donné que les DL sont généralement créés pour résoudre des problèmes spécifiques, la plupart d'entre eux ont au moins deux ou trois applications réelles. En règle générale, les résultats sont très positifs. Les praticiens disent que DL permet de comprendre les problèmes et facilite la recherche de solutions. Pendant longtemps, le principal champion a été Praxis (maintenant Altran), qui a appliqué le «fix-by-design» - une combinaison de constructions en Z et de code SPARK - pour créer des systèmes de sécurité critiques. Les spécifications permettent d'économiser du temps et de l'argent car vous ne trouverez pas d'erreurs de conception à un stade avancé du projet.

Pamela Zave a expérimenté avec Alloy et a découvert un bug fondamental dans Chord, l'une des principales tables de hachage distribuées. AWS commence à rechercher des erreurs critiques en 35 étapesen écrivant les spécifications TLA +. D'après mon expérience, lorsque les gens essaient de rédiger des spécifications, ils deviennent très vite de grands fans de cette entreprise.

Mais les fans de méthodes formelles et les gens de l'extérieur évaluent complètement différemment la valeur de la rédaction des spécifications. Pour les fans, le plus grand avantage est que le processus de conception lui-même vous fait comprendre ce que vous écrivez. Lorsque vous devez exprimer formellement ce que fait votre système, de nombreuses erreurs implicites deviennent soudainement douloureusement évidentes. Les étrangers ne peuvent pas comprendre cela du tout. Si vous voulez donner à quelqu'un un essai DL, une personne devrait avoir un moyen de vérifier que la conception a vraiment les propriétés qu'il souhaite.

Heureusement, cela est également extrêmement important pour de nombreux spécificateurs, de sorte que la vérification de la conception est un vaste domaine de recherche.

Vérification du modèle

Comme pour le code, nous pouvons vérifier la conception en écrivant des théorèmes. Heureusement, nous avons une autre astuce: vous pouvez utiliser le programme de vérification de modèle. Au lieu de compiler des preuves que la conception est correcte, nous forçons simplement l'espace brut des états possibles et voyons si le mauvais état existe en lui. Si nous ne trouvons rien, alors tout va bien (remarque: les programmes de vérification de modèle sont également utilisés pour vérifier le code, comme JMBC, mais la vérification de modèle est beaucoup plus souvent utilisée dans la vérification de conception que la vérification de code).

La validation du modèle présente de nombreux avantages. Premièrement, il n'est pas nécessaire de rédiger des preuves, ce qui économise beaucoup de temps et d'efforts. Deuxièmement, pas besoin d'apprendrerédiger des preuves, de sorte que la barrière d'entrée est beaucoup plus faible. Troisièmement, si la conception est brisée, la vérification du modèle donnera un contre-exemple explicite. Cela rend beaucoup plus facile de corriger l'erreur, surtout s'il faut 35 étapes pour la reproduire. Essayez de le trouver vous-même.

Il y a quelques inconvénients. Tout d'abord, ces outils ne sont pas si puissants. En particulier, vous pouvez rencontrer un nombre illimité (unbounded) , . , : . … , , . , , .

— (state-space explosion). , , , . , (4*3)! / (4!)^3 = 34 650exécutions (comportements) possibles. Si chaque processus a l'un des cinq états initiaux, le nombre total de comportements augmente à 4 300 000. Et la vérification des modèles doit s'assurer qu'ils se comportent tous bien. Et cela à condition qu'ils n'interagissent pas entre eux! S'ils commencent à le faire, l'espace d'état augmentera encore plus rapidement. Une explosion combinatoire est considérée comme le principal problème pour tester des modèles, et beaucoup de travail reste à faire pour résoudre ce problème.

Mais en même temps, il existe une autre façon de faire face à l'explosion de l'espace de l'État: lui jeter plus d'équipement. Le plus gros problème pour vérifier le modèle est «juste» le problème de performance, et nous résolvons très bien les problèmes de performance. La plupart (mais pas tous) les vérifications de modèle sont facilement parallélisées. Après avoir optimisé le modèle et l'avoir testé avec de petits paramètres, vous pouvez déployer le cluster AWS et l'exécuter avec de grands paramètres.

Dans la pratique, de nombreux qualificatifs utilisent la validation du modèle, puis, si nécessaire, passent à des programmes pour prouver les théorèmes (note: gardez à l'esprit que «de nombreux qualificatifs» sont environ dix). Encore plus de compilateurs de spécifications commencent à tester des modèles et lorsqu'ils atteignent la limite de leurs capacités, ils passent à des formes de vérification moins intensives.

Problème de spécification de conception

, , , . ? DV . — , — : .

, — . DL , (: ; . ; , ( ) clarification : des recherches actives sont en cours dans les deux sens).

Les programmeurs ont tendance à se méfier des artefacts logiciels qui ne sont pas du code ou ne sont pas obligés de se synchroniser avec le code. Pour la même raison, la documentation, les commentaires, les graphiques, les wikis et les validations sont souvent ignorés.

Il semble que les programmeurs ne croient tout simplement pas que les spécifications soient utiles. D'après mon expérience, ils suggèrent que les outils actuels (pseudo-code, diagrammes, TDD) sont plus que suffisants pour une bonne conception. Je ne sais pas à quel point cette opinion est répandue et je ne peux pas l'expliquer avec autre chose que le conservatisme général.

Mais exactement chaque communauté de méthodologie a de telles plaintes que je sais: les partisans de TDD se plaignent que les programmeurs ne veulent pas essayer TDD, les fans de Haskell se plaignent que les programmeurs ne pensent pas au typage statique, etc.

J'ai entendu l'argument selon lequel Agile n'accepte pas une conception préconçue, donc personne ne veut faire de spécification formelle. Peut-être. Mais beaucoup de gens que j'ai rencontrés rejettent Agile et FM. Un autre argument est que les méthodes historiquement formelles ont été constamment réévaluées et n'ont pas rempli ce qui avait été promis. C'est également possible, mais la plupart des gens n'ont même pas entendu parler des méthodes formelles, et encore plus de leur histoire.

Il est tout simplement très difficile de faire en sorte que les gens s'inquiètent de ce qu'ils ne font pas encore, même s'ils en reconnaissent les avantages.

Résumé

La vérification du code est une tâche difficile. De plus en plus de personnes s'impliquent, bien que les programmes de démonstration de théorèmes et les solveurs SMT deviennent plus complexes. Mais encore, dans un avenir prévisible, probablement, cela restera le lot de spécialistes.

La vérification de la conception est beaucoup plus simple, mais son utilisation nécessite de surmonter la barrière culturelle. Je pense que la situation peut changer. Il y a vingt ans, les tests automatisés et les révisions de code étaient des sujets assez exotiques et de niche, mais sont finalement devenus courants. Encore une fois, la programmation des contrats était une niche et le reste.

J'espère que cet article explique un peu mieux pourquoi les méthodes formelles sont si rarement utilisées. Au moins, c'est une meilleure explication que l'argument habituel "le web n'est pas un avion". N'hésitez pas à crier si vous voyez des erreurs évidentes.

Pourquoi les gens n'utilisent-ils pas des méthodes formelles?