Exactitude du programme, la spécification

17

De Wikipedia: En informatique théorique, l'exactitude d'un algorithme est affirmée quand on dit que l'algorithme est correct par rapport à une spécification.

Mais le problème est que pour obtenir la spécification "appropriée" n'est pas une tâche triviale, et il n'y a pas de méthode correcte à 100% (pour autant que je sache) pour obtenir la bonne, c'est juste une estimation, donc si nous allons prendre un prédicat comme spécification juste parce qu'il "ressemble" à "l'un", pourquoi ne pas prendre le programme comme correct juste parce qu'il "semble" correct?

Maykel Jakson
la source
2
Parce que j'espère que la spécification est moins compliquée que le programme, donc il y aura moins d'erreurs que le programme.
user253751
1
Notez qu'un système de type est une forme de spécification - nous pouvons l'utiliser pour prouver certaines propriétés non triviales des programmes. Plus le système de caractères est riche, plus les propriétés que nous pouvons prouver sont fortes.
gardenhead
@immibis mais s'il n'y a qu'une seule erreur, tout est faux
Maykel Jakson
@ MaykelJakson Vrai ... J'ai mis une fois une contradiction dans un axiome dans Rodin par erreur (ce que j'essayais de faire était correct mais la syntaxe était erronée). Il m'a fallu un peu de temps «hmm, le prouveur automatique semble fonctionner exceptionnellement bien en ce moment» avant de le remarquer.
user253751

Réponses:

30

Tout d'abord, vous avez tout à fait raison: vous vous inquiétez vraiment. La vérification formelle transfère le problème de la confiance dans l'exactitude du programme au problème de la confiance dans l'exactitude des spécifications, ce n'est donc pas une solution miracle.

Il existe cependant plusieurs raisons pour lesquelles ce processus peut toujours être utile.

  1. Les spécifications sont souvent plus simples que le code lui-même. Par exemple, considérons le problème du tri d'un tableau d'entiers. Il existe des algorithmes de tri assez sophistiqués qui font des choses intelligentes pour améliorer les performances. Mais la spécification est assez simple à énoncer: la sortie doit être en ordre croissant et doit être une permutation de l'entrée. Ainsi, il est sans doute plus facile de gagner en confiance dans l'exactitude de la spécification que dans l'exactitude du code lui-même.

  2. Il n'y a pas de point de défaillance unique. Supposons qu'une personne écrive une spécification et une autre personne écrive le code source, puis vérifie officiellement que le code est conforme à la spécification. Ensuite, tout défaut non détecté devrait être présent à la fois dans la spécification et dans le code. Dans certains cas, pour certains types de défauts, cela semble moins probable: il est moins probable que vous ignoriez le défaut lors de l'inspection de la spécification et que vous ignoriez le défaut lors de l'inspection du code source. Pas tous, mais certains.

  3. Les spécifications partielles peuvent être beaucoup plus simples que le code. Par exemple, considérez l'exigence que le programme soit exempt de vulnérabilités de dépassement de tampon. Ou, l'exigence selon laquelle il n'y a pas d'erreurs hors limites d'index de tableau. Il s'agit d'une simple spécification qui est assez évidemment une bonne chose et utile à prouver. Vous pouvez maintenant essayer d'utiliser des méthodes formelles pour prouver que l'ensemble du programme répond à cette spécification. Cela peut être une tâche assez complexe, mais si vous réussissez, vous gagnez en confiance dans le programme.

  4. Les spécifications peuvent changer moins fréquemment que le code. Sans méthodes formelles, chaque fois que nous mettons à jour le code source, nous devons vérifier manuellement que la mise à jour n'introduira aucun bogue ou défaut. Les méthodes formelles peuvent potentiellement réduire cette charge: supposons que la spécification ne change pas, de sorte que les mises à jour logicielles impliquent uniquement des modifications du code et non des modifications de la spécification. Ensuite, pour chaque mise à jour, vous êtes déchargé de la charge de vérifier si la spécification est toujours correcte (elle n'a pas changé, donc il n'y a aucun risque de nouveaux bogues ont été introduits dans la spécification) et de la charge de vérifier si le code est toujours correct (le vérificateur de programme vérifie cela pour vous). Vous devez toujours vérifier que la spécification d'origine est correcte, mais vous n'avez pas besoin de la vérifier à chaque fois qu'un développeur valide un nouveau correctif / mise à jour / modification.

Enfin, n'oubliez pas que les spécifications sont généralement déclaratives et ne peuvent pas nécessairement être exécutées ni compilées directement en code. Par exemple, envisagez à nouveau de trier: la spécification indique que la sortie augmente et est une permutation de l'entrée, mais il n'y a aucun moyen évident "d'exécuter" cette spécification directement et aucun moyen évident pour un compilateur de la compiler automatiquement en code. Donc, prendre la spécification comme correcte et l'exécuter n'est souvent pas une option.

Néanmoins, le résultat final reste le même: les méthodes formelles ne sont pas une panacée. Ils transfèrent simplement le problème (très difficile) de confiance dans l'exactitude du code au problème (simplement difficile) de confiance dans l'exactitude des spécifications. Les bogues dans la spécification représentent un risque réel, ils sont courants et ne peuvent être négligés. En effet, la communauté des méthodes formelles sépare parfois le problème en deux parties: la vérification consiste à s'assurer que le code répond aux spécifications; la validation consiste à s'assurer que la spécification est correcte (répond à nos besoins).

Vous pouvez également profiter de la vérification formelle du programme dans la pratique et pourquoi ne cherchons-nous pas davantage à compiler les garanties de temps? pour plus de perspectives avec une certaine incidence à ce sujet.

DW
la source
En passant, à mesure qu'une spécification devient plus détaillée, la probabilité qu'elle puisse être écrite lorsque le pseudocode augmente. En utilisant votre exemple de tri, une version plus détaillée de "la sortie doit être en ordre croissant" serait "chaque entier dans la sortie, après le premier, doit être plus grand que le nombre précédent". Ceci, à son tour, peut facilement être écrit comme quelque chose comme for each integer I<sub> N</sub> in set S (where N > 1) { assert I<sub> N</sub> > I<sub> N - 1</sub> }. Pas sûr à 100% de la notation.
Justin Time - Rétablir Monica le
Ainsi, une bonne spécification peut également aider à créer le code, pas seulement à le vérifier.
Justin Time - Rétablir Monica le
1
La manière évidente d'exécuter la spécification de tri est d'énumérer toutes les permutations de l'entrée et de choisir celle qui est ordonnée. Le problème avec ce , bien que, devrait être clair ...
Derek Elkins a
19

La réponse de DW est excellente , mais je voudrais développer un point. Une spécification n'est pas seulement une référence par rapport à laquelle le code est vérifié. L'une des raisons d'avoir une spécification formelle est de la valider en prouvant certaines propriétés fondamentales. Bien sûr, la spécification ne peut pas être complètement validée - la validation serait aussi complexe que la spécification elle-même, ce serait donc un processus sans fin. Mais la validation nous permet d'obtenir une garantie plus forte sur certaines propriétés critiques.

Par exemple, supposons que vous conceviez un pilote automatique de voiture. C'est une chose assez complexe impliquant beaucoup de paramètres. Les propriétés de correction du pilote automatique incluent des choses comme «la voiture ne va pas s'écraser contre un mur» et «la voiture va conduire là où on lui dit d'aller». Une propriété comme «la voiture ne va pas s'écraser contre un mur» est vraiment très importante, nous aimerions donc le prouver. Étant donné que le système fonctionne dans le monde physique, vous devrez ajouter des contraintes physiques; la propriété réelle du système de calcul sera quelque chose comme "sous ces hypothèses concernant la science des matériaux, et ces hypothèses concernant la perception des obstacles par les capteurs de la voiture, la voiture ne va pas s'écraser contre un mur". Mais même ainsi, le résultat est une propriété relativement simple qui est clairement souhaitable.

Pourriez-vous prouver cette propriété à partir du code? En fin de compte, c'est ce qui se passe, si vous suivez une approche entièrement formelle¹. Mais le code a beaucoup de parties différentes; les freins, les caméras, le moteur, etc. sont tous contrôlés de manière autonome. Une propriété de correction des freins serait quelque chose comme «si le signal« appliquer les freins »est activé, alors les freins sont appliqués». Une propriété de correction du moteur serait «si le signal d'embrayage est coupé, alors le moteur ne conduit pas les roues». Il faut une vue de très haut niveau pour les rassembler. Une spécification crée une couche intermédiaire où les différents composants du système peuvent être articulés ensemble.

En fait, un système aussi complexe qu'un pilote automatique de voiture aurait plusieurs niveaux de spécifications avec des quantités variables de raffinements. Une approche de raffinement est souvent utilisée dans la conception: commencez par certaines propriétés de haut niveau comme «la voiture ne va pas s'écraser contre un mur», puis déterminez que cela nécessite des capteurs et des freins et définissez certaines exigences de base pour les capteurs, les freins et le logiciel pilote, puis affiner à nouveau ces exigences de base dans la conception du composant (pour le capteur, je vais avoir besoin d'un radar, d'un DSP, d'une bibliothèque de traitement d'images,…), etc. Dans un processus de développement formel, il est prouvé que chaque niveau de spécification répond aux exigences définies par le niveau supérieur, depuis les propriétés de plus haut niveau jusqu'au code.

Il est impossible d'être sûr que la spécification est correcte. Par exemple, si vous vous trompez de physique, les freins peuvent ne pas être efficaces même si les calculs reliant le code de freinage aux exigences formelles sont corrects. Il ne sert à rien de prouver que les pauses sont efficaces avec 500 kg de charge si vous en avez réellement 5000 kg. Mais il est plus facile de voir que 500 kg est faux que de voir à l'intérieur du code des freins qu'ils ne seront pas assez bons pour les paramètres physiques de la voiture.

¹ Le contraire d'une approche entièrement formelle est «Je suppose que cela fonctionne, mais je ne peux pas en être sûr». Lorsque vous pariez votre vie dessus, cela ne semble pas si bien.

Gilles 'SO- arrête d'être méchant'
la source
Est-il possible de prouver une seule propriété de mon code et de m'assurer qu'elle sera toujours correcte, par exemple, je veux juste prouver que l'index d'un tableau n'est jamais en dehors de la limite du tableau, et je m'en fiche les autres trucs?
Maykel Jakson, le
5
@MaykelJakson Bien sûr! Vous l'utilisez simplement comme spécification. C'est probablement une spécification faible, mais rien ne vous empêche de l'utiliser et d'utiliser des méthodes formelles pour le prouver.
chi