Dans le cadre de mon Bacc en Génie Logiciel je dois suivre le cours Spécification formelle et vérification de logiciels.. et c'est plate.
Pour créer nos spécifications formelles, on utilise Perfect Developer. Un (autre) logiciel qui est supposé faire disparaître les bugs logiciels de la surface de la planète.
Bullshit.
À force de me torturer avec ce merveilleux logiciel (et son tout aussi agréable langage de spécification), j'ai compilé une liste de 5 raisons qui expliquent pourquoi Perfect Developer ne sauvera pas l'humanité des BSOD.
1] La syntaxe
La syntaxe du langage utilisé par Perfect Developer ne ressemble à rien. Si j'avais à désigner un nouveau langage qui s'addresse principalement à des programmeurs, je ferais un effort pour créer un langage similaire à ce qu'ils connaissent déjà.
Ok, ok.. peut-être que les langages qui existent déjà n'offre pas les possibilités dont tu as besoin. Ça ne t'empêche pas de faire un effort d'utilisabilité et de t'arranger pour que tes mots clés soient lisibles. Qu'est-ce qui peut justifier que le not equals soit '~=' ...
En plus, Perfect Developer ne semble pas avoir de concept de variable locale. Ainsi, dans une spécification, il faut tout mettre sur une ligne. Impossbile de capturer une information et la réutiliser à plusieurs places. Il faut copier/coller le code pour obtenir cette information partout où l'on accèderait normalement à la variable locale.
La cerise sur le sunday est qu'il n'y a pas d'IDE. Il faut tout coder dans un editeur texte, pas d'autocomplete.
2] La documentation
Ou plutôt l'absence de documentation. Voici la documentation officielle de Perfect Developer. Je vous invite à porter une attention particulière à l'Annexe A2 qui documente l'API.
Il n'y a rien à comprendre. En fait, pour comprendre la syntaxe, il faut comprendre la syntaxe. Quelle brillante idée. Documentation du langage écrite avec son propre langage. Tu n'explique pas la syntaxe de la langue française à un Chinois avec un document en Français !
Mais tout ça serait acceptable si pour chaque méthode il y avait un exemple. Voici un extrait de la javadoc de la méthode split() de la classe String. On voit que tout est expliqué avec des mots simples. Plusieurs exemples illustrent des cas d'utilisation typiques. Très facile à comprendre, même pour quelqu'un qui n'a aucune idée comment utiliser cette classe ou cette méthode.
Aussi, il n'y a aucune documentation alternative. Pas de blog, pas de registre d'exemples.. rien. Mais c'est peut-être simplement parce que personne n'utilise Perfect Developer ? Je n'aurais pas de difficulté à comprendre ça.
3] L'architecture
La façon dont Perfect Developer gère les intéraction entre les différents objets est très mathématique. On peut faire des opérations telles que l'union de deux ensembles ou l'intersection. Malheureusement, cela implique que pour exprimer l'appartenance, il faut souvent recourir à une relation.
Par exemple, supposons que nous avons une classe Maison et que cette classe possède une liste de Personnes. Une personne possède un nom.
En Java :
class Maison{
List habitants;
}
class Personne{
String nom;
}
En Perfect Developer :
class Maison ^=
var
habitants : map of (Personne -> String);
class Personne ^= tag;
Quel est le problème ?
On n'encapsule pas le nom à l'intérieur de notre classe Personne. Bien sur, il est possible de le faire. Cependant, le problème survient lorsque plus tard on veut spécifier des opérations complexes (Le déménagement d'une personne par exemple). Il devient très difficile et très lourd d'accéder aux données à travers de nombreux niveaux d'encapsulation.
Bref, pour se simplifier la vie, lorsque deux classes ont une relation 1-*, utiliser une map.
Vous ne voudriez pas maintenir un logiciel où tout est une HashMap n'est-ce pas ? Ce n'est pas très orienté objet !
Moi non plus.
4] La vitesse
Grâce à ce superbe langage, écrire une spécification est long et pénible. Mais ce n'est pas le seul problème. Vérifier la spécification est interminable !
J'écris ce post entre 2 vérifications. Et ce n'est pas parce que notre spécification couvre un gros logiciel ! À moins que 3 classes soit un signe que ton logiciel est trop gros ?
La spécification sur laquelle je travaille présentement nécessite plus de 15 minutes à prouver. Les Warnings et les Erreurs n'apparaissent qu'une fois les 15 minutes écoulées. Il n'est donc pas possible de faire progresser le projet durant cette période... et la spécification fait moins de 200 lignes (incluant les commentaires).
Afin de ne pas se donner de chance, Perfect Developer vérifie la spécification en entier, même si seulement une partie minime a changée.
5] La pertinence
Comme vous avez peut-être compris au fur et à mesure de la lecture de ce post.. L'écriture d'une spécification en Perfect Developer nécessite beaucoup de temps, d'effort et de patience. Mais si tout ces efforts servent à complètement éliminer les bugs de votre logiciel, ça vaut la peine, n'est-ce pas ?
Non.
Mais ce n'est pas un "Non ça ne vaut pas la peine d'éliminer tous les bugs". C'est un "Non, ça n'élimine pas tous les bugs". En effet, Perfect Developer ne peut pas garantir que votre code est parfait. Évidemment, la spécification n'est aussi bonne que celui qui l'écrit. Il peut y avoir des bugs dans votre spécification (belle ironie).
En ayant à tout coder 2 fois (Une fois pour écrire la spécification et une autre fois pour coder le logiciel), on double les chances de créer des bugs. On augmente également les coûts de production.
Ok, ok, supposons que nous avons quelqu'un qui maitrise vraiment bien le langage. On peut s'attendre à ce que la spécification crée par cette personne donnera une bonne garantie de l'absence de bug dans notre logiciel. On peut donc s'attendre à ce que ceux qui ont développé Perfect Developer aient les connaissances nécessaires afin de produire une spécification blindée.
On peut lire sur le FAQ de Perfect Developer :
There would be no point in selling a product to generate bug-free code if it contained bugs itself, therefore nearly all of Perfect Developer is implemented in its own technology.
Donc un des arguments de vente du produit est "Notre produit à pas de bug puisque nous l'avons certifié avec notre produit qui élimine les bugs". À part la faille flagrante de logique circulaire, il y a quelque chose de fondamentalement faux dans cet argument.
Internal error: rewrote using illegal branch combination! Please submit your example to Escher Technologies.
Perfect Developer a des bugs. En effet, ma spécification compile. Je sais que la logique est bonne. Cependant, elle fait planter le logiciel. À tous les coups !
Bravo Escher Technologies.
Je penses que ça démontre bien l'inutilité de tout ça. Leur logiciel est spécifié par Perfect Developer. Ils connaissent bien leurs outils. Il y a quand même des bugs. Les spécifications formelles n'en valent pas la peine.
Conclusion
Je trouve que les spécifications formelles sont un beau sujet de recherche. Il est facile de voir l'attrait ! Éliminer complètement les chances d'obtenir des bugs ?
Malheureusement, je crois que le temps investit sur la spécification formelle ne vaut pas la peine. Mieux vaut compter sur la compétence des développeurs et sur d'autres filets de sécurité comme les tests d'acceptation et les tests fonctionnels.
Le manque d'outil est également à blamer. Si seulement il était possible de vérifier une spécification en un temps raisonnable sans avoir un Super-Computer.
.. Dites moi ce que vous en pensez dans les Commentaires !
3 commentaires:
J'exige que les arguments de ce texte soient validés par un vérificateur de preuve!
:P
C'est l'histoire de mon bacc, des cours où l'on nous montre des choses totalement inutiles. Les profs veulent absolument nous montrer leur sujet d'étude ultra-théorique qui risque fort probablement d'aboutir à... rien.
Y peut ben y avoir du décrochage scolaire. Combien de personnes dans le monde utilisent des outils comme perfect developer régulièrement? 50? Dont 49 sont des profs et l'autre essaye de le hacker? Que dire des automates à pile?
Bref, je trouve que tu as ben raison :)
Hi Guisim, I'm sorry you have not found Perfect Developer to your liking. We recognise that the documentation could be improved, but we also provide examples and tutorials (see the self-help page on our support site). Regarding your other comments: (1) The not-equals operator is "~=", not "=~". The symbol "~" always means "not" in PD, hence you can also use ~<, ~> and so on. (2) Of course you can declare local names - in fact, you can declare them anywhere in an expression. For example, you can express X to the power 4 as (let X2 ^= X*X; X2*X2). (3) We don't explain the syntax of Perfect in Perfect, it is the library API that we express in Perfect. This is a very natural thing to do - in particular, it shows you all the preconditions. How many API documents do you know that tell you all the preconditions that you must satisfy when calling them? (4) Of course you can create a House class containing a list of inhabitants - although a set would be more appropriate unless you want to impose an ordering on the inhabitants. (5) There are places in PD itself where we can't prove everything is correct, so we have some run-time checks in those places - hence the "illegal branch combination" check that you unfortunately came across. Had you reported this to us (as the message asks you to), we would have supplied you with a patch or workaround. (6) You can control the prover timeouts in the Verification settings tab. You can also tell PD to run the prover at reduced priority. We provide this specifically so that if you are using a single-processor computer, you can carry on editing specifications etc. with good responsiveness. (7) Formal specifications are far from being just a research topic - they have been used for many years in developing highly critical software, such as fly-by-wire aircraft control systems. Would you really want to fly in an aircraft whose critical software was developed using traditional and more error-prone techniques?
Hi David !
Thanks for taking the time to reply to my post.
I think most of my complaints come down to documentation. As a student, it often felt too complex and unintuitive.
Also, in the context of a single course, It's hard to see how PD can help developing highly critical software. Most of the time, it felt like a complete test suite ( Unit and application-level tests ) would do the same job with less of a hassle.
You response is a very interesting read. If I have to develop a highly critical application, I'll consider using PD.
Enregistrer un commentaire